Thm*  x: , n:  . ((x mod n) mod n) = (x mod n) | [mod_mod] |
| Thm* n:. (n mod n) = 0 | [mod_self] |
Thm* n:  . (n rem n) = 0 | [rem_self] |
| Thm* x,y:, n:. ((x+y) mod n) = (((x mod n)+(y mod n)) mod n) | [mod_add] |
Thm* x,y:, n:. ((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y <  0) (0 < (((x rem n)+(y rem n)) rem n)) -|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi | [rem_add] |
| Thm* x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi | [mod_minus] |
| Thm* x:, n:. ((-x) rem n) = -(x rem n) | [rem_minus] |
| Thm* n:. (0 mod n) = 0 | [zero_mod] |
| Thm* n:. (0 rem n) = 0 | [zero_rem] |
Thm* x,y:, n:. ((x y) mod n) = (((x mod n)(y mod n)) mod n) | [mod_mul] |
| Thm* x,y:, n:. ((xy) rem n) = (((x rem n)(y rem n)) rem n) | [rem_mul] |
Thm* a:, n:, q:, r:. a = qn+r   r < n q = (a   n) & r = (a mod n) | [div_floor_mod_unique] |
| Thm* a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n) | [div_rem_unique] |
| Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n | [div_floor_mod_properties] |
| Thm* a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0) | [div_rem_properties] |
Thm* i:. f91(i)  | [f91_wf] |
| Thm* i:. f91(i) ~ if 101 < i i-10 else 91 fi | [f91-val] |
Thm* k1,k2:.  f:((k1+k2)  (k1+k2)). Inj(k1+k2; (k1+k2); f) | [union_cardinality1] |
| Thm* n:, f:(n). increasing(f;n) (i:n, j:i. f(j) (f(i))) | [increasing-implies2] |
| Thm* f:(AB), g:(BC). Inj(A; B; f) Inj(B; C; g) Inj(A; C; g o f) | [compose_inject] |
| Thm* n:, a,b:. sum(a+bi | i < n) = ((n(a+a+b(n-1))) 2) | [sum_arith] |
| Thm* n:, a,b:. sum(a+bi | i < n)2 = n(a+a+b(n-1)) | [sum_arith1] |
Thm* k:, f,g:(k), p:(k ). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) | [sum-ite] |
Thm* k,b:, f:(k). (x:k. b f(x)) bksum(f(x) | x < k) | [sum_lower_bound] |
| Thm* k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)bk | [sum_bound] |
| Thm* k:, f,g:(k). (x:k. f(x)g(x)) sum(f(x) | x < k)sum(g(x) | x < k) | [sum_le] |
| Thm* a,b:. |ab| = |a||b| | [absval_mul] |
Thm* n:, P:((n+1)Prop). (x:(n+1). P(x))  P(0) & (x:n. P(x+1)) | [all-nsub-add1] |
| Thm* L:(A+B) List, a:A. mapoutl(L) = [a] (L1,L2:(A+B) List. L = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil) | [mapoutl_is_singleton] |
| Thm* L:(A+B) List, l1,l2:A List. mapoutl(L) = (l1 @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2) | [mapoutl_is_append] |
| Thm* L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2)) | [mapoutl_append] |
| Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s)) | [no_repeats_mapoutl] |
| Thm* s:(A+B) List, x:A. (x mapoutl(s)) (inl(x) s) | [mapoutl_member] |
| Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) | [member_mapoutl] |
| Thm* A,B:Type, s:(A+B) List. mapoutl(s) A List | [mapoutl_wf] |
| Thm* f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L) | [list_accum_filter] |
| Thm* i,j:. no_repeats(;upto(i;j)) | [no_repeats_upto] |
Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T.  (x A) & (x B)) ||A|| < ||B|| | [length_less] |
| Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||||B|| | [length_le] |
| Thm* L:T List. no_repeats(T;rev(L)) no_repeats(T;L) | [no_repeats_reverse] |
| Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) | [no_repeats_append_iff] |
| Thm* a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b) | [l_disjoint_append2] |
| Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c) | [l_disjoint_append] |
| Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a) | [l_disjoint_cons2] |
| Thm* a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b) | [l_disjoint_cons] |
| Thm* t:T. no_repeats(T;[t]) | [no_repeats_singleton] |
| Thm* s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f)) | [no_repeats_inj] |
| Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y L f(x) before f(y) mapfilter(f;P;L) | [mapfilter_before] |
| Thm* f:(TT'), x,y:T, s:T List. x before y s f(x) before f(y) map(f;s) | [map_before] |
| Thm* L:T List, x,y:T. x before y L (L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3)) | [l_before-iff] |
Thm* x,z,y,w:T List. ||x|| = ||z||  ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w | [append_one_one] |
| Thm* a,b:T List, x:T. [x] = (a @ b) a = nil & b = [x] b = nil & a = [x] | [append_is_singleton] |
| Thm* a,c,b,d:T List. (a @ b) = (c @ d) (e:T List. a = (c @ e) & d = (e @ b) c = (a @ e) & b = (e @ d)) | [equal_appends] |
| Thm* x:T, L:T List. (x rev(L)) (x L) | [member_reverse] |
| Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1) | [filter_list_accum] |
| Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c) | [append_assoc_sq] |
| Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n)) | [primrec_list_accum] |
| Thm* R:(AA'Prop), P:(BA), P':(BA'), F,G,H:(BAA), F',G',H':(BA'A'), N:(BA(B List)), N':(BA'(B List)), M:(A), M':(A'). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (i:B, s:A'. P'(i,s) M'(F'(i,s))M'(s)) (i:B, s:A'. M'(G'(i,s))M'(s)) (i:B, s:A'. P'(i,s) M'(H'(i,s)) < M'(s)) (j:B, u:A, v:A'. R(u,v) (P(j,u) P'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(F(j,u),F'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(H(j,u),H'(j,v))) (j:B, u:A, v:A'. R(u,v) R(G(j,u),G'(j,v))) (j:B, u:A, v:A'. R(u,v) N(j,u) = N'(j,v)) (j:B, u:A, v:A'. R(u,v) R(process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ,process v j where process s i == if P'(i,s) then F'(i,s) else G'(i,s) where xs := N'(i,s); s:= H'(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } )) | [accumulate-rel] |
| Thm* M:(A), Q:(BAAProp), P:(BA), F,G,H:(BAA), N:(BA(B List)). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. P(j,u) Q(j,u,F(j,u))) (j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))) (j:B, u:A. Q(j,u,u)) (i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)) (j:B, u:A. Q(j,u,process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } )) | [accumulate-induction1] |
| Thm* A,B:Type, P:(BA), F,G,H:(BAA), N:(BA(B List)), M:(A). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } {s:A| M(s)M(u) }) | [accumulate_wf] |
| Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T' | [list_accum_wf] |
| Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B)) | [l_before_decomp] |
| Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B) | [l_before_append_iff] |
Thm* C,A,B:T List. C  A @ B (A',B':T List. C = (A' @ B') & A' A & B' B) | [sublist_append_iff] |
| Thm* (x,y:T. Dec(x = y)) (s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]) & (z s1))) | [l_member_decomp2] |
| Thm* s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2])) | [l_member_decomp] |
| Thm* l1,l2:Top List, f,y:Top. list_accum(x,a.f(x,a);y;l1 @ l2) ~ list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;l1);l2) | [list_accum_append] |
| Thm* L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ L | [append_firstn_lastn_sq] |
| Thm* x,y,z:T List. (x @ z) = (y @ z) x = y | [equal_append_front] |
| Thm* l1,l2:T List. nil = (l1 @ l2) l1 = nil & l2 = nil | [nil_is_append] |
| Thm* f,g:Top, s:Top List. map(f;map(g;s)) ~ map(f o g;s) | [map-map] |
| Thm* s:T List. 0 < ||s|| (s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]])) | [list-decomp-last] |
| Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g)) | [inverse-biject] |
| Thm* f:(AB), g:(BC). Bij(A; B; f) Bij(B; C; g) Bij(A; C; g o f) | [compose-biject] |
| Thm* Bij(T; T; Id) | [identity-biject] |
Thm* g:(AB C). (Id,Id) o g = g | [comp2_id_l] |
| Thm* h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h | [comp2_comp2_assoc] |
| Thm* h:(A'A), g:(ABC), f1:(BB'), f2:(CC'). (f1,f2) o g o h = (f1,f2) o g o h | [comp2_comp_assoc] |
| Thm* x,y:A+B. (a1,a2:A. Dec(a1 = a2)) (b1,b2:B. Dec(b1 = b2)) Dec(x = y) | [decidable__equal_union] |
| Thm* i,j,k:. ij jk (upto(i;k) ~ (upto(i;j) @ upto(j;k))) | [append_upto] |
| Thm* i,j:, k:(j-i). upto(i;j)[k] = i+k | [select_upto] |
| Thm* j:, i:j. ||upto(i;j)|| = j-i | [length_upto] |
| Thm* i,j,k:. (k upto(i;j)) ik & k < j | [member_upto] |
| Thm* i,j:. upto(i;j) List | [upto_int_wf] |
| Thm* i,j:. upto(i;j) {i..j} List | [upto_wf] |
| Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L1,L2:T List. mapfilter(f;P;L1 @ L2) = (mapfilter(f;P;L1) @ mapfilter(f;P;L2)) | [mapfilter_append] |
| Thm* x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3 | [equal_appends_eq] |
| Thm* x1,z,x2,x3:T List. ||z||||x1|| (x1 @ x2) = (z @ x3) (z':T List. x1 = (z @ z') & x3 = (z' @ x2)) | [equal_appends_case2] |
| Thm* x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3)) | [equal_appends_case1] |
| Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_bexists] |
| Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_ball] |