API tools faq
paste
Advertisement
Guest User

Untitled

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