API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 19th, 2017
56
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml 48.18 KB | None | 0 0
raw download clone embed print report
  1. let make_base_cime prog input output =
  2.   ignore(Sys.command
  3.         (Printf.sprintf "%s -itrs %s -ocime %s > %s" prog input output output)
  4.   )
  5.  
  6. let compute prog input output constraints =
  7.   make_base_cime prog input output;
  8.   let chan =
  9.     open_out_gen
  10.       [Open_wronly;Open_append]
  11.       0
  12.       output
  13.   in
  14.   output_string chan "#Set_sat_solver \"minisat2\";\n";
  15.   output_string chan "#verbose 4 ;\n";
  16.   let constraints_definition =
  17.     Printf.sprintf "let c = order_constraints R_trs_0_algebra \"%s\" ;\n" constraints
  18.   in
  19.   output_string chan constraints_definition;
  20.   output_string chan "ordering_solve false c ;\n";
  21.   ignore(Sys.command
  22.       (Printf.sprintf "%s -icime %s" prog output)
  23.   )
  24.  
  25.  
  26. let R_trs_0_variable =  variables "V,M,V1,IL,V2,L,N,X" ;
  27. let R_trs_0_signature =
  28.  signature "isNatKind : 1; isNatIList : 1; length : 1; U22 : 1; take : 2;
  29.  U31 : 2; U62 : 2; U12 : 1; and : 2; U41 : 3; U63 : 1; U11 : 2; nil : 0;
  30.  U21 : 2; U51 : 3; 0 : 0; isNatIListKind : 1; U43 : 1; s : 1; tt : 0;
  31.  U81 : 1; U32 : 1; U53 : 1; zeros : 0; U91 : 4; U42 : 2; U61 : 3;
  32.  isNatList : 1; U71 : 2; isNat : 1; U52 : 2; cons : 2" ;
  33. let R_trs_0_algebra =  algebra R_trs_0_signature ;
  34. let R_trs_0 =
  35.  trs R_trs_0_algebra "
  36.   zeros -> cons(0,zeros);
  37.  
  38.   U11(tt,V1) -> U12(isNatList(V1));
  39.  
  40.   U12(tt) -> tt;
  41.  
  42.   U21(tt,V1) -> U22(isNat(V1));
  43.  
  44.   U22(tt) -> tt;
  45.  
  46.   U31(tt,V) -> U32(isNatList(V));
  47.  
  48.   U32(tt) -> tt;
  49.  
  50.   U41(tt,V1,V2) -> U42(isNat(V1),V2);
  51.  
  52.   U42(tt,V2) -> U43(isNatIList(V2));
  53.  
  54.   U43(tt) -> tt;
  55.  
  56.   U51(tt,V1,V2) -> U52(isNat(V1),V2);
  57.  
  58.   U52(tt,V2) -> U53(isNatList(V2));
  59.  
  60.   U53(tt) -> tt;
  61.  
  62.   U61(tt,V1,V2) -> U62(isNat(V1),V2);
  63.  
  64.   U62(tt,V2) -> U63(isNatIList(V2));
  65.  
  66.   U63(tt) -> tt;
  67.  
  68.   U71(tt,L) -> s(length(L));
  69.  
  70.   U81(tt) -> nil;
  71.  
  72.   U91(tt,IL,M,N) -> cons(N,take(M,IL));
  73.  
  74.   and(tt,X) -> X;
  75.  
  76.   isNat(0) -> tt;
  77.  
  78.   isNat(length(V1)) -> U11(isNatIListKind(V1),V1);
  79.  
  80.   isNat(s(V1)) -> U21(isNatKind(V1),V1);
  81.  
  82.   isNatIList(V) -> U31(isNatIListKind(V),V);
  83.  
  84.   isNatIList(zeros) -> tt;
  85.  
  86.   isNatIList(cons(V1,V2)) -> U41(and(isNatKind(V1),isNatIListKind(V2)),V1,V2);
  87.  
  88.   isNatIListKind(nil) -> tt;
  89.  
  90.   isNatIListKind(zeros) -> tt;
  91.  
  92.   isNatIListKind(cons(V1,V2)) -> and(isNatKind(V1),isNatIListKind(V2));
  93.  
  94.   isNatIListKind(take(V1,V2)) -> and(isNatKind(V1),isNatIListKind(V2));
  95.  
  96.   isNatKind(0) -> tt;
  97.  
  98.   isNatKind(length(V1)) -> isNatIListKind(V1);
  99.  
  100.   isNatKind(s(V1)) -> isNatKind(V1);
  101.  
  102.   isNatList(nil) -> tt;
  103.  
  104.   isNatList(cons(V1,V2)) -> U51(and(isNatKind(V1),isNatIListKind(V2)),V1,V2);
  105.  
  106.   isNatList(take(V1,V2)) -> U61(and(isNatKind(V1),isNatIListKind(V2)),V1,V2);
  107.  
  108.   length(nil) -> 0;
  109.  
  110.   length(cons(N,L))
  111.    -> U71(and(and(isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),
  112.        L);
  113.  
  114.   take(0,IL) -> U81(and(isNatIList(IL),isNatIListKind(IL)));
  115.  
  116.   take(s(M),cons(N,IL))
  117.    -> U91(and(and(isNatIList(IL),isNatIListKind(IL)),
  118.            and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))),
  119.        IL,M,N)
  120.  " ;
  121. #Set_sat_solver "minisat2";
  122. #verbose 4 ;
  123. let c = order_constraints R_trs_0_algebra " zeros >= zeros
  124. /\  (
  125.         zeros > zeros
  126.     )
  127. /\  zeros >= cons(0, zeros)
  128.  
  129. /\
  130.  
  131.     take(s(M), cons(N, IL)) >= U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
  132. /\  U91(tt, IL, M, N) >= take(M, IL)
  133. /\  (
  134.         take(s(M), cons(N, IL)) > U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
  135.     \/  U91(tt, IL, M, N) > take(M, IL)
  136.     )
  137. /\  U11(tt, V1) >= U12(isNatList(V1))
  138. /\  U12(tt) >= tt
  139. /\  U21(tt, V1) >= U22(isNat(V1))
  140. /\  U22(tt) >= tt
  141. /\  U31(tt, V) >= U32(isNatList(V))
  142. /\  U32(tt) >= tt
  143. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  144. /\  U42(tt, V2) >= U43(isNatIList(V2))
  145. /\  U43(tt) >= tt
  146. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  147. /\  U52(tt, V2) >= U53(isNatList(V2))
  148. /\  U53(tt) >= tt
  149. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  150. /\  U62(tt, V2) >= U63(isNatIList(V2))
  151. /\  U63(tt) >= tt
  152. /\  U81(tt) >= nil
  153. /\  U91(tt, IL, M, N) >= cons(N, take(M, IL))
  154. /\  and(tt, X) >= X
  155. /\  isNat(0) >= tt
  156. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  157. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  158. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  159. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  160. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  161. /\  isNatIListKind(nil) >= tt
  162. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  163. /\  isNatKind(0) >= tt
  164. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  165. /\  isNatKind(s(V1)) >= isNatKind(V1)
  166. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  167. /\  isNatList(nil) >= tt
  168. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  169. /\  take(0, IL) >= U81(and(isNatIList(IL), isNatIListKind(IL)))
  170. /\  take(s(M), cons(N, IL)) >= U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
  171.  
  172. /\
  173.  
  174.     take(s(M), cons(N, IL)) >= isNatKind(N)
  175. /\  (
  176.         take(s(M), cons(N, IL)) > isNatKind(N)
  177.     )
  178. /\  and(tt, X) >= X
  179. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  180. /\  isNatIListKind(nil) >= tt
  181. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  182. /\  isNatKind(0) >= tt
  183. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  184. /\  isNatKind(s(V1)) >= isNatKind(V1)
  185.  
  186. /\
  187.  
  188.     take(s(M), cons(N, IL)) >= isNatKind(M)
  189. /\  (
  190.         take(s(M), cons(N, IL)) > isNatKind(M)
  191.     )
  192. /\  and(tt, X) >= X
  193. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  194. /\  isNatIListKind(nil) >= tt
  195. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  196. /\  isNatKind(0) >= tt
  197. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  198. /\  isNatKind(s(V1)) >= isNatKind(V1)
  199.  
  200. /\
  201.  
  202.     take(s(M), cons(N, IL)) >= isNatIListKind(IL)
  203. /\  (
  204.         take(s(M), cons(N, IL)) > isNatIListKind(IL)
  205.     )
  206. /\  and(tt, X) >= X
  207. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  208. /\  isNatIListKind(nil) >= tt
  209. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  210. /\  isNatKind(0) >= tt
  211. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  212. /\  isNatKind(s(V1)) >= isNatKind(V1)
  213.  
  214. /\
  215.  
  216.     take(s(M), cons(N, IL)) >= isNatIList(IL)
  217. /\  (
  218.         take(s(M), cons(N, IL)) > isNatIList(IL)
  219.     )
  220. /\  U11(tt, V1) >= U12(isNatList(V1))
  221. /\  U12(tt) >= tt
  222. /\  U21(tt, V1) >= U22(isNat(V1))
  223. /\  U22(tt) >= tt
  224. /\  U31(tt, V) >= U32(isNatList(V))
  225. /\  U32(tt) >= tt
  226. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  227. /\  U42(tt, V2) >= U43(isNatIList(V2))
  228. /\  U43(tt) >= tt
  229. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  230. /\  U52(tt, V2) >= U53(isNatList(V2))
  231. /\  U53(tt) >= tt
  232. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  233. /\  U62(tt, V2) >= U63(isNatIList(V2))
  234. /\  U63(tt) >= tt
  235. /\  and(tt, X) >= X
  236. /\  isNat(0) >= tt
  237. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  238. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  239. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  240. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  241. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  242. /\  isNatIListKind(nil) >= tt
  243. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  244. /\  isNatKind(0) >= tt
  245. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  246. /\  isNatKind(s(V1)) >= isNatKind(V1)
  247. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  248. /\  isNatList(nil) >= tt
  249. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  250.  
  251. /\
  252.  
  253.     take(s(M), cons(N, IL)) >= isNat(N)
  254. /\  (
  255.         take(s(M), cons(N, IL)) > isNat(N)
  256.     )
  257. /\  U11(tt, V1) >= U12(isNatList(V1))
  258. /\  U12(tt) >= tt
  259. /\  U21(tt, V1) >= U22(isNat(V1))
  260. /\  U22(tt) >= tt
  261. /\  U31(tt, V) >= U32(isNatList(V))
  262. /\  U32(tt) >= tt
  263. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  264. /\  U42(tt, V2) >= U43(isNatIList(V2))
  265. /\  U43(tt) >= tt
  266. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  267. /\  U52(tt, V2) >= U53(isNatList(V2))
  268. /\  U53(tt) >= tt
  269. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  270. /\  U62(tt, V2) >= U63(isNatIList(V2))
  271. /\  U63(tt) >= tt
  272. /\  and(tt, X) >= X
  273. /\  isNat(0) >= tt
  274. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  275. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  276. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  277. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  278. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  279. /\  isNatIListKind(nil) >= tt
  280. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  281. /\  isNatKind(0) >= tt
  282. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  283. /\  isNatKind(s(V1)) >= isNatKind(V1)
  284. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  285. /\  isNatList(nil) >= tt
  286. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  287.  
  288. /\
  289.  
  290.     take(s(M), cons(N, IL)) >= isNat(M)
  291. /\  (
  292.         take(s(M), cons(N, IL)) > isNat(M)
  293.     )
  294. /\  U11(tt, V1) >= U12(isNatList(V1))
  295. /\  U12(tt) >= tt
  296. /\  U21(tt, V1) >= U22(isNat(V1))
  297. /\  U22(tt) >= tt
  298. /\  U31(tt, V) >= U32(isNatList(V))
  299. /\  U32(tt) >= tt
  300. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  301. /\  U42(tt, V2) >= U43(isNatIList(V2))
  302. /\  U43(tt) >= tt
  303. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  304. /\  U52(tt, V2) >= U53(isNatList(V2))
  305. /\  U53(tt) >= tt
  306. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  307. /\  U62(tt, V2) >= U63(isNatIList(V2))
  308. /\  U63(tt) >= tt
  309. /\  and(tt, X) >= X
  310. /\  isNat(0) >= tt
  311. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  312. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  313. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  314. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  315. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  316. /\  isNatIListKind(nil) >= tt
  317. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  318. /\  isNatKind(0) >= tt
  319. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  320. /\  isNatKind(s(V1)) >= isNatKind(V1)
  321. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  322. /\  isNatList(nil) >= tt
  323. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  324.  
  325. /\
  326.  
  327.     take(s(M), cons(N, IL)) >= and(isNatIList(IL), isNatIListKind(IL))
  328. /\  (
  329.         take(s(M), cons(N, IL)) > and(isNatIList(IL), isNatIListKind(IL))
  330.     )
  331. /\  U11(tt, V1) >= U12(isNatList(V1))
  332. /\  U12(tt) >= tt
  333. /\  U21(tt, V1) >= U22(isNat(V1))
  334. /\  U22(tt) >= tt
  335. /\  U31(tt, V) >= U32(isNatList(V))
  336. /\  U32(tt) >= tt
  337. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  338. /\  U42(tt, V2) >= U43(isNatIList(V2))
  339. /\  U43(tt) >= tt
  340. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  341. /\  U52(tt, V2) >= U53(isNatList(V2))
  342. /\  U53(tt) >= tt
  343. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  344. /\  U62(tt, V2) >= U63(isNatIList(V2))
  345. /\  U63(tt) >= tt
  346. /\  and(tt, X) >= X
  347. /\  isNat(0) >= tt
  348. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  349. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  350. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  351. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  352. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  353. /\  isNatIListKind(nil) >= tt
  354. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  355. /\  isNatKind(0) >= tt
  356. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  357. /\  isNatKind(s(V1)) >= isNatKind(V1)
  358. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  359. /\  isNatList(nil) >= tt
  360. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  361.  
  362. /\
  363.  
  364.     take(s(M), cons(N, IL)) >= and(isNat(N), isNatKind(N))
  365. /\  (
  366.         take(s(M), cons(N, IL)) > and(isNat(N), isNatKind(N))
  367.     )
  368. /\  U11(tt, V1) >= U12(isNatList(V1))
  369. /\  U12(tt) >= tt
  370. /\  U21(tt, V1) >= U22(isNat(V1))
  371. /\  U22(tt) >= tt
  372. /\  U31(tt, V) >= U32(isNatList(V))
  373. /\  U32(tt) >= tt
  374. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  375. /\  U42(tt, V2) >= U43(isNatIList(V2))
  376. /\  U43(tt) >= tt
  377. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  378. /\  U52(tt, V2) >= U53(isNatList(V2))
  379. /\  U53(tt) >= tt
  380. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  381. /\  U62(tt, V2) >= U63(isNatIList(V2))
  382. /\  U63(tt) >= tt
  383. /\  and(tt, X) >= X
  384. /\  isNat(0) >= tt
  385. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  386. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  387. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  388. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  389. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  390. /\  isNatIListKind(nil) >= tt
  391. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  392. /\  isNatKind(0) >= tt
  393. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  394. /\  isNatKind(s(V1)) >= isNatKind(V1)
  395. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  396. /\  isNatList(nil) >= tt
  397. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  398.  
  399. /\
  400.  
  401.     take(s(M), cons(N, IL)) >= and(isNat(M), isNatKind(M))
  402. /\  (
  403.         take(s(M), cons(N, IL)) > and(isNat(M), isNatKind(M))
  404.     )
  405. /\  U11(tt, V1) >= U12(isNatList(V1))
  406. /\  U12(tt) >= tt
  407. /\  U21(tt, V1) >= U22(isNat(V1))
  408. /\  U22(tt) >= tt
  409. /\  U31(tt, V) >= U32(isNatList(V))
  410. /\  U32(tt) >= tt
  411. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  412. /\  U42(tt, V2) >= U43(isNatIList(V2))
  413. /\  U43(tt) >= tt
  414. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  415. /\  U52(tt, V2) >= U53(isNatList(V2))
  416. /\  U53(tt) >= tt
  417. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  418. /\  U62(tt, V2) >= U63(isNatIList(V2))
  419. /\  U63(tt) >= tt
  420. /\  and(tt, X) >= X
  421. /\  isNat(0) >= tt
  422. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  423. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  424. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  425. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  426. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  427. /\  isNatIListKind(nil) >= tt
  428. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  429. /\  isNatKind(0) >= tt
  430. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  431. /\  isNatKind(s(V1)) >= isNatKind(V1)
  432. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  433. /\  isNatList(nil) >= tt
  434. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  435.  
  436. /\
  437.  
  438.     take(s(M), cons(N, IL)) >= and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))))
  439. /\  (
  440.         take(s(M), cons(N, IL)) > and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))))
  441.     )
  442. /\  U11(tt, V1) >= U12(isNatList(V1))
  443. /\  U12(tt) >= tt
  444. /\  U21(tt, V1) >= U22(isNat(V1))
  445. /\  U22(tt) >= tt
  446. /\  U31(tt, V) >= U32(isNatList(V))
  447. /\  U32(tt) >= tt
  448. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  449. /\  U42(tt, V2) >= U43(isNatIList(V2))
  450. /\  U43(tt) >= tt
  451. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  452. /\  U52(tt, V2) >= U53(isNatList(V2))
  453. /\  U53(tt) >= tt
  454. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  455. /\  U62(tt, V2) >= U63(isNatIList(V2))
  456. /\  U63(tt) >= tt
  457. /\  and(tt, X) >= X
  458. /\  isNat(0) >= tt
  459. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  460. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  461. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  462. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  463. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  464. /\  isNatIListKind(nil) >= tt
  465. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  466. /\  isNatKind(0) >= tt
  467. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  468. /\  isNatKind(s(V1)) >= isNatKind(V1)
  469. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  470. /\  isNatList(nil) >= tt
  471. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  472.  
  473. /\
  474.  
  475.     take(s(M), cons(N, IL)) >= and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
  476. /\  (
  477.         take(s(M), cons(N, IL)) > and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
  478.     )
  479. /\  U11(tt, V1) >= U12(isNatList(V1))
  480. /\  U12(tt) >= tt
  481. /\  U21(tt, V1) >= U22(isNat(V1))
  482. /\  U22(tt) >= tt
  483. /\  U31(tt, V) >= U32(isNatList(V))
  484. /\  U32(tt) >= tt
  485. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  486. /\  U42(tt, V2) >= U43(isNatIList(V2))
  487. /\  U43(tt) >= tt
  488. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  489. /\  U52(tt, V2) >= U53(isNatList(V2))
  490. /\  U53(tt) >= tt
  491. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  492. /\  U62(tt, V2) >= U63(isNatIList(V2))
  493. /\  U63(tt) >= tt
  494. /\  and(tt, X) >= X
  495. /\  isNat(0) >= tt
  496. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  497. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  498. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  499. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  500. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  501. /\  isNatIListKind(nil) >= tt
  502. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  503. /\  isNatKind(0) >= tt
  504. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  505. /\  isNatKind(s(V1)) >= isNatKind(V1)
  506. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  507. /\  isNatList(nil) >= tt
  508. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  509.  
  510. /\
  511.  
  512.     take(0, IL) >= isNatIListKind(IL)
  513. /\  (
  514.         take(0, IL) > isNatIListKind(IL)
  515.     )
  516. /\  and(tt, X) >= X
  517. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  518. /\  isNatIListKind(nil) >= tt
  519. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  520. /\  isNatKind(0) >= tt
  521. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  522. /\  isNatKind(s(V1)) >= isNatKind(V1)
  523.  
  524. /\
  525.  
  526.     take(0, IL) >= isNatIList(IL)
  527. /\  (
  528.         take(0, IL) > isNatIList(IL)
  529.     )
  530. /\  U11(tt, V1) >= U12(isNatList(V1))
  531. /\  U12(tt) >= tt
  532. /\  U21(tt, V1) >= U22(isNat(V1))
  533. /\  U22(tt) >= tt
  534. /\  U31(tt, V) >= U32(isNatList(V))
  535. /\  U32(tt) >= tt
  536. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  537. /\  U42(tt, V2) >= U43(isNatIList(V2))
  538. /\  U43(tt) >= tt
  539. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  540. /\  U52(tt, V2) >= U53(isNatList(V2))
  541. /\  U53(tt) >= tt
  542. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  543. /\  U62(tt, V2) >= U63(isNatIList(V2))
  544. /\  U63(tt) >= tt
  545. /\  and(tt, X) >= X
  546. /\  isNat(0) >= tt
  547. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  548. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  549. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  550. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  551. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  552. /\  isNatIListKind(nil) >= tt
  553. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  554. /\  isNatKind(0) >= tt
  555. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  556. /\  isNatKind(s(V1)) >= isNatKind(V1)
  557. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  558. /\  isNatList(nil) >= tt
  559. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  560.  
  561. /\
  562.  
  563.     take(0, IL) >= and(isNatIList(IL), isNatIListKind(IL))
  564. /\  (
  565.         take(0, IL) > and(isNatIList(IL), isNatIListKind(IL))
  566.     )
  567. /\  U11(tt, V1) >= U12(isNatList(V1))
  568. /\  U12(tt) >= tt
  569. /\  U21(tt, V1) >= U22(isNat(V1))
  570. /\  U22(tt) >= tt
  571. /\  U31(tt, V) >= U32(isNatList(V))
  572. /\  U32(tt) >= tt
  573. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  574. /\  U42(tt, V2) >= U43(isNatIList(V2))
  575. /\  U43(tt) >= tt
  576. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  577. /\  U52(tt, V2) >= U53(isNatList(V2))
  578. /\  U53(tt) >= tt
  579. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  580. /\  U62(tt, V2) >= U63(isNatIList(V2))
  581. /\  U63(tt) >= tt
  582. /\  and(tt, X) >= X
  583. /\  isNat(0) >= tt
  584. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  585. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  586. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  587. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  588. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  589. /\  isNatIListKind(nil) >= tt
  590. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  591. /\  isNatKind(0) >= tt
  592. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  593. /\  isNatKind(s(V1)) >= isNatKind(V1)
  594. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  595. /\  isNatList(nil) >= tt
  596. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  597.  
  598. /\
  599.  
  600.     take(0, IL) >= U81(and(isNatIList(IL), isNatIListKind(IL)))
  601. /\  (
  602.         take(0, IL) > U81(and(isNatIList(IL), isNatIListKind(IL)))
  603.     )
  604. /\  U11(tt, V1) >= U12(isNatList(V1))
  605. /\  U12(tt) >= tt
  606. /\  U21(tt, V1) >= U22(isNat(V1))
  607. /\  U22(tt) >= tt
  608. /\  U31(tt, V) >= U32(isNatList(V))
  609. /\  U32(tt) >= tt
  610. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  611. /\  U42(tt, V2) >= U43(isNatIList(V2))
  612. /\  U43(tt) >= tt
  613. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  614. /\  U52(tt, V2) >= U53(isNatList(V2))
  615. /\  U53(tt) >= tt
  616. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  617. /\  U62(tt, V2) >= U63(isNatIList(V2))
  618. /\  U63(tt) >= tt
  619. /\  U81(tt) >= nil
  620. /\  and(tt, X) >= X
  621. /\  isNat(0) >= tt
  622. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  623. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  624. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  625. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  626. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  627. /\  isNatIListKind(nil) >= tt
  628. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  629. /\  isNatKind(0) >= tt
  630. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  631. /\  isNatKind(s(V1)) >= isNatKind(V1)
  632. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  633. /\  isNatList(nil) >= tt
  634. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  635.  
  636. /\
  637.  
  638.     length(cons(N, L)) >= U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
  639. /\  U71(tt, L) >= length(L)
  640. /\  (
  641.         length(cons(N, L)) > U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
  642.     \/  U71(tt, L) > length(L)
  643.     )
  644. /\  U11(tt, V1) >= U12(isNatList(V1))
  645. /\  U12(tt) >= tt
  646. /\  U21(tt, V1) >= U22(isNat(V1))
  647. /\  U22(tt) >= tt
  648. /\  U31(tt, V) >= U32(isNatList(V))
  649. /\  U32(tt) >= tt
  650. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  651. /\  U42(tt, V2) >= U43(isNatIList(V2))
  652. /\  U43(tt) >= tt
  653. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  654. /\  U52(tt, V2) >= U53(isNatList(V2))
  655. /\  U53(tt) >= tt
  656. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  657. /\  U62(tt, V2) >= U63(isNatIList(V2))
  658. /\  U63(tt) >= tt
  659. /\  U71(tt, L) >= s(length(L))
  660. /\  and(tt, X) >= X
  661. /\  isNat(0) >= tt
  662. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  663. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  664. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  665. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  666. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  667. /\  isNatIListKind(nil) >= tt
  668. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  669. /\  isNatKind(0) >= tt
  670. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  671. /\  isNatKind(s(V1)) >= isNatKind(V1)
  672. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  673. /\  isNatList(nil) >= tt
  674. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  675. /\  length(cons(N, L)) >= U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
  676. /\  length(nil) >= 0
  677.  
  678. /\
  679.  
  680.     length(cons(N, L)) >= isNatList(L)
  681. /\  (
  682.         length(cons(N, L)) > isNatList(L)
  683.     )
  684. /\  U11(tt, V1) >= U12(isNatList(V1))
  685. /\  U12(tt) >= tt
  686. /\  U21(tt, V1) >= U22(isNat(V1))
  687. /\  U22(tt) >= tt
  688. /\  U31(tt, V) >= U32(isNatList(V))
  689. /\  U32(tt) >= tt
  690. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  691. /\  U42(tt, V2) >= U43(isNatIList(V2))
  692. /\  U43(tt) >= tt
  693. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  694. /\  U52(tt, V2) >= U53(isNatList(V2))
  695. /\  U53(tt) >= tt
  696. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  697. /\  U62(tt, V2) >= U63(isNatIList(V2))
  698. /\  U63(tt) >= tt
  699. /\  and(tt, X) >= X
  700. /\  isNat(0) >= tt
  701. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  702. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  703. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  704. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  705. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  706. /\  isNatIListKind(nil) >= tt
  707. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  708. /\  isNatKind(0) >= tt
  709. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  710. /\  isNatKind(s(V1)) >= isNatKind(V1)
  711. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  712. /\  isNatList(nil) >= tt
  713. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  714.  
  715. /\
  716.  
  717.     length(cons(N, L)) >= isNatKind(N)
  718. /\  (
  719.         length(cons(N, L)) > isNatKind(N)
  720.     )
  721. /\  and(tt, X) >= X
  722. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  723. /\  isNatIListKind(nil) >= tt
  724. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  725. /\  isNatKind(0) >= tt
  726. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  727. /\  isNatKind(s(V1)) >= isNatKind(V1)
  728.  
  729. /\
  730.  
  731.     length(cons(N, L)) >= isNatIListKind(L)
  732. /\  (
  733.         length(cons(N, L)) > isNatIListKind(L)
  734.     )
  735. /\  and(tt, X) >= X
  736. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  737. /\  isNatIListKind(nil) >= tt
  738. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  739. /\  isNatKind(0) >= tt
  740. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  741. /\  isNatKind(s(V1)) >= isNatKind(V1)
  742.  
  743. /\
  744.  
  745.     length(cons(N, L)) >= isNat(N)
  746. /\  (
  747.         length(cons(N, L)) > isNat(N)
  748.     )
  749. /\  U11(tt, V1) >= U12(isNatList(V1))
  750. /\  U12(tt) >= tt
  751. /\  U21(tt, V1) >= U22(isNat(V1))
  752. /\  U22(tt) >= tt
  753. /\  U31(tt, V) >= U32(isNatList(V))
  754. /\  U32(tt) >= tt
  755. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  756. /\  U42(tt, V2) >= U43(isNatIList(V2))
  757. /\  U43(tt) >= tt
  758. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  759. /\  U52(tt, V2) >= U53(isNatList(V2))
  760. /\  U53(tt) >= tt
  761. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  762. /\  U62(tt, V2) >= U63(isNatIList(V2))
  763. /\  U63(tt) >= tt
  764. /\  and(tt, X) >= X
  765. /\  isNat(0) >= tt
  766. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  767. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  768. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  769. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  770. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  771. /\  isNatIListKind(nil) >= tt
  772. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  773. /\  isNatKind(0) >= tt
  774. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  775. /\  isNatKind(s(V1)) >= isNatKind(V1)
  776. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  777. /\  isNatList(nil) >= tt
  778. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  779.  
  780. /\
  781.  
  782.     length(cons(N, L)) >= and(isNatList(L), isNatIListKind(L))
  783. /\  (
  784.         length(cons(N, L)) > and(isNatList(L), isNatIListKind(L))
  785.     )
  786. /\  U11(tt, V1) >= U12(isNatList(V1))
  787. /\  U12(tt) >= tt
  788. /\  U21(tt, V1) >= U22(isNat(V1))
  789. /\  U22(tt) >= tt
  790. /\  U31(tt, V) >= U32(isNatList(V))
  791. /\  U32(tt) >= tt
  792. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  793. /\  U42(tt, V2) >= U43(isNatIList(V2))
  794. /\  U43(tt) >= tt
  795. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  796. /\  U52(tt, V2) >= U53(isNatList(V2))
  797. /\  U53(tt) >= tt
  798. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  799. /\  U62(tt, V2) >= U63(isNatIList(V2))
  800. /\  U63(tt) >= tt
  801. /\  and(tt, X) >= X
  802. /\  isNat(0) >= tt
  803. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  804. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  805. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  806. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  807. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  808. /\  isNatIListKind(nil) >= tt
  809. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  810. /\  isNatKind(0) >= tt
  811. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  812. /\  isNatKind(s(V1)) >= isNatKind(V1)
  813. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  814. /\  isNatList(nil) >= tt
  815. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  816.  
  817. /\
  818.  
  819.     length(cons(N, L)) >= and(isNat(N), isNatKind(N))
  820. /\  (
  821.         length(cons(N, L)) > and(isNat(N), isNatKind(N))
  822.     )
  823. /\  U11(tt, V1) >= U12(isNatList(V1))
  824. /\  U12(tt) >= tt
  825. /\  U21(tt, V1) >= U22(isNat(V1))
  826. /\  U22(tt) >= tt
  827. /\  U31(tt, V) >= U32(isNatList(V))
  828. /\  U32(tt) >= tt
  829. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  830. /\  U42(tt, V2) >= U43(isNatIList(V2))
  831. /\  U43(tt) >= tt
  832. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  833. /\  U52(tt, V2) >= U53(isNatList(V2))
  834. /\  U53(tt) >= tt
  835. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  836. /\  U62(tt, V2) >= U63(isNatIList(V2))
  837. /\  U63(tt) >= tt
  838. /\  and(tt, X) >= X
  839. /\  isNat(0) >= tt
  840. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  841. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  842. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  843. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  844. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  845. /\  isNatIListKind(nil) >= tt
  846. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  847. /\  isNatKind(0) >= tt
  848. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  849. /\  isNatKind(s(V1)) >= isNatKind(V1)
  850. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  851. /\  isNatList(nil) >= tt
  852. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  853.  
  854. /\
  855.  
  856.     length(cons(N, L)) >= and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
  857. /\  (
  858.         length(cons(N, L)) > and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
  859.     )
  860. /\  U11(tt, V1) >= U12(isNatList(V1))
  861. /\  U12(tt) >= tt
  862. /\  U21(tt, V1) >= U22(isNat(V1))
  863. /\  U22(tt) >= tt
  864. /\  U31(tt, V) >= U32(isNatList(V))
  865. /\  U32(tt) >= tt
  866. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  867. /\  U42(tt, V2) >= U43(isNatIList(V2))
  868. /\  U43(tt) >= tt
  869. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  870. /\  U52(tt, V2) >= U53(isNatList(V2))
  871. /\  U53(tt) >= tt
  872. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  873. /\  U62(tt, V2) >= U63(isNatIList(V2))
  874. /\  U63(tt) >= tt
  875. /\  and(tt, X) >= X
  876. /\  isNat(0) >= tt
  877. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  878. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  879. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  880. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  881. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  882. /\  isNatIListKind(nil) >= tt
  883. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  884. /\  isNatKind(0) >= tt
  885. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  886. /\  isNatKind(s(V1)) >= isNatKind(V1)
  887. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  888. /\  isNatList(nil) >= tt
  889. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  890.  
  891. /\
  892.  
  893.     isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  894. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  895. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  896. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  897. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  898. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  899. /\  U62(tt, V2) >= isNatIList(V2)
  900. /\  U61(tt, V1, V2) >= isNat(V1)
  901. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  902. /\  U52(tt, V2) >= isNatList(V2)
  903. /\  U51(tt, V1, V2) >= isNat(V1)
  904. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  905. /\  U42(tt, V2) >= isNatIList(V2)
  906. /\  U41(tt, V1, V2) >= isNat(V1)
  907. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  908. /\  U31(tt, V) >= isNatList(V)
  909. /\  U21(tt, V1) >= isNat(V1)
  910. /\  U11(tt, V1) >= isNatList(V1)
  911. /\  (
  912.         isNatList(take(V1, V2)) > U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  913.     \/  isNatList(cons(V1, V2)) > U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  914.     \/  isNatIList(cons(V1, V2)) > U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  915.     \/  isNatIList(V) > U31(isNatIListKind(V), V)
  916.     \/  isNat(s(V1)) > U21(isNatKind(V1), V1)
  917.     \/  isNat(length(V1)) > U11(isNatIListKind(V1), V1)
  918.     \/  U62(tt, V2) > isNatIList(V2)
  919.     \/  U61(tt, V1, V2) > isNat(V1)
  920.     \/  U61(tt, V1, V2) > U62(isNat(V1), V2)
  921.     \/  U52(tt, V2) > isNatList(V2)
  922.     \/  U51(tt, V1, V2) > isNat(V1)
  923.     \/  U51(tt, V1, V2) > U52(isNat(V1), V2)
  924.     \/  U42(tt, V2) > isNatIList(V2)
  925.     \/  U41(tt, V1, V2) > isNat(V1)
  926.     \/  U41(tt, V1, V2) > U42(isNat(V1), V2)
  927.     \/  U31(tt, V) > isNatList(V)
  928.     \/  U21(tt, V1) > isNat(V1)
  929.     \/  U11(tt, V1) > isNatList(V1)
  930.     )
  931. /\  U11(tt, V1) >= U12(isNatList(V1))
  932. /\  U12(tt) >= tt
  933. /\  U21(tt, V1) >= U22(isNat(V1))
  934. /\  U22(tt) >= tt
  935. /\  U31(tt, V) >= U32(isNatList(V))
  936. /\  U32(tt) >= tt
  937. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  938. /\  U42(tt, V2) >= U43(isNatIList(V2))
  939. /\  U43(tt) >= tt
  940. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  941. /\  U52(tt, V2) >= U53(isNatList(V2))
  942. /\  U53(tt) >= tt
  943. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  944. /\  U62(tt, V2) >= U63(isNatIList(V2))
  945. /\  U63(tt) >= tt
  946. /\  and(tt, X) >= X
  947. /\  isNat(0) >= tt
  948. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  949. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  950. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  951. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  952. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  953. /\  isNatIListKind(nil) >= tt
  954. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  955. /\  isNatKind(0) >= tt
  956. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  957. /\  isNatKind(s(V1)) >= isNatKind(V1)
  958. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  959. /\  isNatList(nil) >= tt
  960. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  961.  
  962. /\
  963.  
  964.     isNat(s(V1)) >= isNatKind(V1)
  965. /\  (
  966.         isNat(s(V1)) > isNatKind(V1)
  967.     )
  968. /\  and(tt, X) >= X
  969. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  970. /\  isNatIListKind(nil) >= tt
  971. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  972. /\  isNatKind(0) >= tt
  973. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  974. /\  isNatKind(s(V1)) >= isNatKind(V1)
  975.  
  976. /\
  977.  
  978.     U21(tt, V1) >= U22(isNat(V1))
  979. /\  (
  980.         U21(tt, V1) > U22(isNat(V1))
  981.     )
  982. /\  U11(tt, V1) >= U12(isNatList(V1))
  983. /\  U12(tt) >= tt
  984. /\  U21(tt, V1) >= U22(isNat(V1))
  985. /\  U22(tt) >= tt
  986. /\  U31(tt, V) >= U32(isNatList(V))
  987. /\  U32(tt) >= tt
  988. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  989. /\  U42(tt, V2) >= U43(isNatIList(V2))
  990. /\  U43(tt) >= tt
  991. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  992. /\  U52(tt, V2) >= U53(isNatList(V2))
  993. /\  U53(tt) >= tt
  994. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  995. /\  U62(tt, V2) >= U63(isNatIList(V2))
  996. /\  U63(tt) >= tt
  997. /\  and(tt, X) >= X
  998. /\  isNat(0) >= tt
  999. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  1000. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  1001. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  1002. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1003. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1004. /\  isNatIListKind(nil) >= tt
  1005. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1006. /\  isNatKind(0) >= tt
  1007. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1008. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1009. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1010. /\  isNatList(nil) >= tt
  1011. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1012.  
  1013. /\
  1014.  
  1015.     isNat(length(V1)) >= isNatIListKind(V1)
  1016. /\  (
  1017.         isNat(length(V1)) > isNatIListKind(V1)
  1018.     )
  1019. /\  and(tt, X) >= X
  1020. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1021. /\  isNatIListKind(nil) >= tt
  1022. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1023. /\  isNatKind(0) >= tt
  1024. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1025. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1026.  
  1027. /\
  1028.  
  1029.     isNatIList(cons(V1, V2)) >= isNatKind(V1)
  1030. /\  (
  1031.         isNatIList(cons(V1, V2)) > isNatKind(V1)
  1032.     )
  1033. /\  and(tt, X) >= X
  1034. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1035. /\  isNatIListKind(nil) >= tt
  1036. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1037. /\  isNatKind(0) >= tt
  1038. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1039. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1040.  
  1041. /\
  1042.  
  1043.     isNatIList(cons(V1, V2)) >= isNatIListKind(V2)
  1044. /\  (
  1045.         isNatIList(cons(V1, V2)) > isNatIListKind(V2)
  1046.     )
  1047. /\  and(tt, X) >= X
  1048. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1049. /\  isNatIListKind(nil) >= tt
  1050. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1051. /\  isNatKind(0) >= tt
  1052. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1053. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1054.  
  1055. /\
  1056.  
  1057.     isNatIList(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1058. /\  (
  1059.         isNatIList(cons(V1, V2)) > and(isNatKind(V1), isNatIListKind(V2))
  1060.     )
  1061. /\  and(tt, X) >= X
  1062. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1063. /\  isNatIListKind(nil) >= tt
  1064. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1065. /\  isNatKind(0) >= tt
  1066. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1067. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1068.  
  1069. /\
  1070.  
  1071.     U42(tt, V2) >= U43(isNatIList(V2))
  1072. /\  (
  1073.         U42(tt, V2) > U43(isNatIList(V2))
  1074.     )
  1075. /\  U11(tt, V1) >= U12(isNatList(V1))
  1076. /\  U12(tt) >= tt
  1077. /\  U21(tt, V1) >= U22(isNat(V1))
  1078. /\  U22(tt) >= tt
  1079. /\  U31(tt, V) >= U32(isNatList(V))
  1080. /\  U32(tt) >= tt
  1081. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  1082. /\  U42(tt, V2) >= U43(isNatIList(V2))
  1083. /\  U43(tt) >= tt
  1084. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  1085. /\  U52(tt, V2) >= U53(isNatList(V2))
  1086. /\  U53(tt) >= tt
  1087. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  1088. /\  U62(tt, V2) >= U63(isNatIList(V2))
  1089. /\  U63(tt) >= tt
  1090. /\  and(tt, X) >= X
  1091. /\  isNat(0) >= tt
  1092. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  1093. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  1094. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  1095. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1096. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1097. /\  isNatIListKind(nil) >= tt
  1098. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1099. /\  isNatKind(0) >= tt
  1100. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1101. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1102. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1103. /\  isNatList(nil) >= tt
  1104. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1105.  
  1106. /\
  1107.  
  1108.     isNatIList(V) >= isNatIListKind(V)
  1109. /\  (
  1110.         isNatIList(V) > isNatIListKind(V)
  1111.     )
  1112. /\  and(tt, X) >= X
  1113. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1114. /\  isNatIListKind(nil) >= tt
  1115. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1116. /\  isNatKind(0) >= tt
  1117. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1118. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1119.  
  1120. /\
  1121.  
  1122.     isNatList(take(V1, V2)) >= isNatKind(V1)
  1123. /\  (
  1124.         isNatList(take(V1, V2)) > isNatKind(V1)
  1125.     )
  1126. /\  and(tt, X) >= X
  1127. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1128. /\  isNatIListKind(nil) >= tt
  1129. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1130. /\  isNatKind(0) >= tt
  1131. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1132. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1133.  
  1134. /\
  1135.  
  1136.     isNatList(take(V1, V2)) >= isNatIListKind(V2)
  1137. /\  (
  1138.         isNatList(take(V1, V2)) > isNatIListKind(V2)
  1139.     )
  1140. /\  and(tt, X) >= X
  1141. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1142. /\  isNatIListKind(nil) >= tt
  1143. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1144. /\  isNatKind(0) >= tt
  1145. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1146. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1147.  
  1148. /\
  1149.  
  1150.     isNatList(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1151. /\  (
  1152.         isNatList(take(V1, V2)) > and(isNatKind(V1), isNatIListKind(V2))
  1153.     )
  1154. /\  and(tt, X) >= X
  1155. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1156. /\  isNatIListKind(nil) >= tt
  1157. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1158. /\  isNatKind(0) >= tt
  1159. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1160. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1161.  
  1162. /\
  1163.  
  1164.     U31(tt, V) >= U32(isNatList(V))
  1165. /\  (
  1166.         U31(tt, V) > U32(isNatList(V))
  1167.     )
  1168. /\  U11(tt, V1) >= U12(isNatList(V1))
  1169. /\  U12(tt) >= tt
  1170. /\  U21(tt, V1) >= U22(isNat(V1))
  1171. /\  U22(tt) >= tt
  1172. /\  U31(tt, V) >= U32(isNatList(V))
  1173. /\  U32(tt) >= tt
  1174. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  1175. /\  U42(tt, V2) >= U43(isNatIList(V2))
  1176. /\  U43(tt) >= tt
  1177. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  1178. /\  U52(tt, V2) >= U53(isNatList(V2))
  1179. /\  U53(tt) >= tt
  1180. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  1181. /\  U62(tt, V2) >= U63(isNatIList(V2))
  1182. /\  U63(tt) >= tt
  1183. /\  and(tt, X) >= X
  1184. /\  isNat(0) >= tt
  1185. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  1186. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  1187. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  1188. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1189. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1190. /\  isNatIListKind(nil) >= tt
  1191. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1192. /\  isNatKind(0) >= tt
  1193. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1194. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1195. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1196. /\  isNatList(nil) >= tt
  1197. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1198.  
  1199. /\
  1200.  
  1201.     U62(tt, V2) >= U63(isNatIList(V2))
  1202. /\  (
  1203.         U62(tt, V2) > U63(isNatIList(V2))
  1204.     )
  1205. /\  U11(tt, V1) >= U12(isNatList(V1))
  1206. /\  U12(tt) >= tt
  1207. /\  U21(tt, V1) >= U22(isNat(V1))
  1208. /\  U22(tt) >= tt
  1209. /\  U31(tt, V) >= U32(isNatList(V))
  1210. /\  U32(tt) >= tt
  1211. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  1212. /\  U42(tt, V2) >= U43(isNatIList(V2))
  1213. /\  U43(tt) >= tt
  1214. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  1215. /\  U52(tt, V2) >= U53(isNatList(V2))
  1216. /\  U53(tt) >= tt
  1217. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  1218. /\  U62(tt, V2) >= U63(isNatIList(V2))
  1219. /\  U63(tt) >= tt
  1220. /\  and(tt, X) >= X
  1221. /\  isNat(0) >= tt
  1222. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  1223. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  1224. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  1225. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1226. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1227. /\  isNatIListKind(nil) >= tt
  1228. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1229. /\  isNatKind(0) >= tt
  1230. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1231. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1232. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1233. /\  isNatList(nil) >= tt
  1234. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1235.  
  1236. /\
  1237.  
  1238.     isNatList(cons(V1, V2)) >= isNatKind(V1)
  1239. /\  (
  1240.         isNatList(cons(V1, V2)) > isNatKind(V1)
  1241.     )
  1242. /\  and(tt, X) >= X
  1243. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1244. /\  isNatIListKind(nil) >= tt
  1245. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1246. /\  isNatKind(0) >= tt
  1247. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1248. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1249.  
  1250. /\
  1251.  
  1252.     isNatList(cons(V1, V2)) >= isNatIListKind(V2)
  1253. /\  (
  1254.         isNatList(cons(V1, V2)) > isNatIListKind(V2)
  1255.     )
  1256. /\  and(tt, X) >= X
  1257. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1258. /\  isNatIListKind(nil) >= tt
  1259. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1260. /\  isNatKind(0) >= tt
  1261. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1262. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1263.  
  1264. /\
  1265.  
  1266.     isNatKind(s(V1)) >= isNatKind(V1)
  1267. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1268. /\  isNatIListKind(take(V1, V2)) >= isNatKind(V1)
  1269. /\  isNatIListKind(take(V1, V2)) >= isNatIListKind(V2)
  1270. /\  isNatIListKind(cons(V1, V2)) >= isNatKind(V1)
  1271. /\  isNatIListKind(cons(V1, V2)) >= isNatIListKind(V2)
  1272. /\  (
  1273.         isNatKind(s(V1)) > isNatKind(V1)
  1274.     \/  isNatKind(length(V1)) > isNatIListKind(V1)
  1275.     \/  isNatIListKind(take(V1, V2)) > isNatKind(V1)
  1276.     \/  isNatIListKind(take(V1, V2)) > isNatIListKind(V2)
  1277.     \/  isNatIListKind(cons(V1, V2)) > isNatKind(V1)
  1278.     \/  isNatIListKind(cons(V1, V2)) > isNatIListKind(V2)
  1279.     )
  1280. /\  and(tt, X) >= X
  1281. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1282. /\  isNatIListKind(nil) >= tt
  1283. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1284. /\  isNatKind(0) >= tt
  1285. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1286. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1287.  
  1288. /\
  1289.  
  1290.     isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1291. /\  (
  1292.         isNatIListKind(take(V1, V2)) > and(isNatKind(V1), isNatIListKind(V2))
  1293.     )
  1294. /\  and(tt, X) >= X
  1295. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1296. /\  isNatIListKind(nil) >= tt
  1297. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1298. /\  isNatKind(0) >= tt
  1299. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1300. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1301.  
  1302. /\
  1303.  
  1304.     isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1305. /\  (
  1306.         isNatIListKind(cons(V1, V2)) > and(isNatKind(V1), isNatIListKind(V2))
  1307.     )
  1308. /\  and(tt, X) >= X
  1309. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1310. /\  isNatIListKind(nil) >= tt
  1311. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1312. /\  isNatKind(0) >= tt
  1313. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1314. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1315.  
  1316. /\
  1317.  
  1318.     isNatList(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1319. /\  (
  1320.         isNatList(cons(V1, V2)) > and(isNatKind(V1), isNatIListKind(V2))
  1321.     )
  1322. /\  and(tt, X) >= X
  1323. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1324. /\  isNatIListKind(nil) >= tt
  1325. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1326. /\  isNatKind(0) >= tt
  1327. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1328. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1329.  
  1330. /\
  1331.  
  1332.     U52(tt, V2) >= U53(isNatList(V2))
  1333. /\  (
  1334.         U52(tt, V2) > U53(isNatList(V2))
  1335.     )
  1336. /\  U11(tt, V1) >= U12(isNatList(V1))
  1337. /\  U12(tt) >= tt
  1338. /\  U21(tt, V1) >= U22(isNat(V1))
  1339. /\  U22(tt) >= tt
  1340. /\  U31(tt, V) >= U32(isNatList(V))
  1341. /\  U32(tt) >= tt
  1342. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  1343. /\  U42(tt, V2) >= U43(isNatIList(V2))
  1344. /\  U43(tt) >= tt
  1345. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  1346. /\  U52(tt, V2) >= U53(isNatList(V2))
  1347. /\  U53(tt) >= tt
  1348. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  1349. /\  U62(tt, V2) >= U63(isNatIList(V2))
  1350. /\  U63(tt) >= tt
  1351. /\  and(tt, X) >= X
  1352. /\  isNat(0) >= tt
  1353. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  1354. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  1355. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  1356. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1357. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1358. /\  isNatIListKind(nil) >= tt
  1359. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1360. /\  isNatKind(0) >= tt
  1361. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1362. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1363. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1364. /\  isNatList(nil) >= tt
  1365. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1366.  
  1367. /\
  1368.  
  1369.     U11(tt, V1) >= U12(isNatList(V1))
  1370. /\  (
  1371.         U11(tt, V1) > U12(isNatList(V1))
  1372.     )
  1373. /\  U11(tt, V1) >= U12(isNatList(V1))
  1374. /\  U12(tt) >= tt
  1375. /\  U21(tt, V1) >= U22(isNat(V1))
  1376. /\  U22(tt) >= tt
  1377. /\  U31(tt, V) >= U32(isNatList(V))
  1378. /\  U32(tt) >= tt
  1379. /\  U41(tt, V1, V2) >= U42(isNat(V1), V2)
  1380. /\  U42(tt, V2) >= U43(isNatIList(V2))
  1381. /\  U43(tt) >= tt
  1382. /\  U51(tt, V1, V2) >= U52(isNat(V1), V2)
  1383. /\  U52(tt, V2) >= U53(isNatList(V2))
  1384. /\  U53(tt) >= tt
  1385. /\  U61(tt, V1, V2) >= U62(isNat(V1), V2)
  1386. /\  U62(tt, V2) >= U63(isNatIList(V2))
  1387. /\  U63(tt) >= tt
  1388. /\  and(tt, X) >= X
  1389. /\  isNat(0) >= tt
  1390. /\  isNat(length(V1)) >= U11(isNatIListKind(V1), V1)
  1391. /\  isNat(s(V1)) >= U21(isNatKind(V1), V1)
  1392. /\  isNatIList(V) >= U31(isNatIListKind(V), V)
  1393. /\  isNatIList(cons(V1, V2)) >= U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1394. /\  isNatIListKind(cons(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1395. /\  isNatIListKind(nil) >= tt
  1396. /\  isNatIListKind(take(V1, V2)) >= and(isNatKind(V1), isNatIListKind(V2))
  1397. /\  isNatKind(0) >= tt
  1398. /\  isNatKind(length(V1)) >= isNatIListKind(V1)
  1399. /\  isNatKind(s(V1)) >= isNatKind(V1)
  1400. /\  isNatList(cons(V1, V2)) >= U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
  1401. /\  isNatList(nil) >= tt
  1402. /\  isNatList(take(V1, V2)) >= U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)" ;
  1403. ordering_solve false c ;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!