Selected Objects

def	l_ball	(xL.P(x)) == reduce(x,b. P(x)b;true;L)
def	l_bexists	(xL.P(x)) == reduce(x,b. P(x) b;false;L)
THM	assert_l_ball	L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))
THM	assert_l_bexists	L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))
THM	equal_appends_case1	x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3))
THM	equal_appends_case2	x1,z,x2,x3:T List. ||z||||x1|| (x1 @ x2) = (z @ x3) (z':T List. x1 = (z @ z') & x3 = (z' @ x2))
THM	equal_appends_eq	x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3
THM	mapfilter_append	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))
def	upto	(rec) upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi
THM	member_upto	i,j,k:. (k upto(i;j)) ik & k < j
THM	length_upto	j:, i:j. ||upto(i;j)|| = j-i
THM	select_upto	i,j:, k:(j-i). upto(i;j)[k] = i+k
THM	append_upto	i,j,k:. ij jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))
THM	decidable__equal_union	x,y:A+B. (a1,a2:A. Dec(a1 = a2)) (b1,b2:B. Dec(b1 = b2)) Dec(x = y)
def	union-reduce	union-reduce(f;g;x;as) == reduce(a,y. InjCase(a; j. f(j,y), g(j,y));x;as)
def	plambda	Macro < x,y > .P(x;y)(p) == P(1of(p);2of(p))
def	compose2	(f1,f2) o g(x) == g(x)/x,y. < f1(x),f2(y) >
THM	comp2_comp_assoc	h:(A'A), g:(ABC), f1:(BB'), f2:(CC'). (f1,f2) o g o h = (f1,f2) o g o h
THM	comp2_comp2_assoc	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
THM	comp2_id_l	g:(ABC). (Id,Id) o g = g
THM	identity-biject	Bij(T; T; Id)
THM	compose-biject	f:(AB), g:(BC). Bij(A; B; f) Bij(B; C; g) Bij(A; C; g o f)
THM	inverse-biject	f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))
THM	list-decomp-last	s:T List. 0 < ||s|| (s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]]))
THM	map-map	f,g:Top, s:Top List. map(f;map(g;s)) ~ map(f o g;s)
THM	nil_is_append	l1,l2:T List. nil = (l1 @ l2) l1 = nil & l2 = nil
THM	equal_append_front	x,y,z:T List. (x @ z) = (y @ z) x = y
THM	append_firstn_lastn_sq	L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ L
THM	list_accum_append	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)
def	accumulate	(rec) 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; } == if P(j;u) F(j;u) else G(j;list_accum(s',i'.process s' i' 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; } ;H(j;u);N(j;u))) fi
THM	l_member_decomp	s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]))
THM	l_member_decomp2	(x,y:T. Dec(x = y)) (s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]) & (z s1)))
THM	sublist_append_iff	C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B)
THM	l_before_append_iff	A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)
THM	l_before_decomp	L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B))
THM	accumulate-induction1	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; } ))
THM	accumulate-rel	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; } ))
THM	primrec_list_accum	n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))
THM	append_assoc_sq	a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c)
THM	filter_list_accum	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)
THM	member_reverse	x:T, L:T List. (x rev(L)) (x L)
THM	equal_appends	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))
THM	append_is_singleton	a,b:T List, x:T. [x] = (a @ b) a = nil & b = [x] b = nil & a = [x]
THM	append_one_one	x,z,y,w:T List. ||x|| = ||z|| ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w
THM	l_before-iff	L:T List, x,y:T. x before y L (L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3))
THM	map_before	f:(TT'), x,y:T, s:T List. x before y s f(x) before f(y) map(f;s)
THM	mapfilter_before	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)
THM	no_repeats_inj	s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f))
THM	no_repeats_singleton	t:T. no_repeats(T;[t])
THM	l_disjoint_cons	a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b)
THM	l_disjoint_cons2	a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a)
THM	l_disjoint_append	a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c)
THM	l_disjoint_append2	a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b)
THM	no_repeats_append_iff	l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)
THM	no_repeats_reverse	L:T List. no_repeats(T;rev(L)) no_repeats(T;L)
THM	length_le	A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||||B||
THM	length_less	A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) ||A|| < ||B||
THM	no_repeats_upto	i,j:. no_repeats(;upto(i;j))
THM	list_accum_filter	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)
def	mapoutl	mapoutl(s) == mapfilter(x.outl(x);x.isl(x);s)
THM	member_mapoutl	s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y))
THM	mapoutl_member	s:(A+B) List, x:A. (x mapoutl(s)) (inl(x) s)
THM	no_repeats_mapoutl	s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))
THM	mapoutl_append	L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2))
THM	mapoutl_is_append	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)
THM	mapoutl_is_singleton	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)
THM	all-nsub-add1	n:, P:((n+1)Prop). (x:(n+1). P(x)) P(0) & (x:n. P(x+1))
THM	absval_mul	a,b:. |ab| = |a||b|
THM	sum_le	k:, f,g:(k). (x:k. f(x)g(x)) sum(f(x) | x < k)sum(g(x) | x < k)
THM	sum_bound	k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)bk
THM	sum_lower_bound	k,b:, f:(k). (x:k. bf(x)) bksum(f(x) | x < k)
THM	sum-ite	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)
THM	sum_arith1	n:, a,b:. sum(a+bi | i < n)2 = n(a+a+b(n-1))
THM	sum_arith	n:, a,b:. sum(a+bi | i < n) = ((n(a+a+b(n-1))) 2)
THM	compose_inject	f:(AB), g:(BC). Inj(A; B; f) Inj(B; C; g) Inj(A; C; g o f)
THM	increasing-implies2	n:, f:(n). increasing(f;n) (i:n, j:i. f(j) (f(i)))
THM	union_cardinality1	k1,k2:. f:((k1+k2)(k1+k2)). Inj(k1+k2; (k1+k2); f)
def	f91	(rec) f91(i) == if 100 < i i-10 else f91(f91(i+11)) fi
THM	f91-val	i:. f91(i) ~ if 101 < i i-10 else 91 fi
THM	div_rem_properties	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)
THM	div_floor_mod_properties	a:, n:. a = (a n)n+(a mod n) & (a mod n) < n
THM	div_rem_unique	a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n)
THM	div_floor_mod_unique	a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n)
THM	rem_mul	x,y:, n:. ((xy) rem n) = (((x rem n)(y rem n)) rem n)
THM	mod_mul	x,y:, n:. ((xy) mod n) = (((x mod n)(y mod n)) mod n)
THM	zero_rem	n:. (0 rem n) = 0
THM	zero_mod	n:. (0 mod n) = 0
THM	rem_minus	x:, n:. ((-x) rem n) = -(x rem n)
THM	mod_minus	x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi
THM	rem_add	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
THM	mod_add	x,y:, n:. ((x+y) mod n) = (((x mod n)+(y mod n)) mod n)
THM	rem_self	n:. (n rem n) = 0
THM	mod_self	n:. (n mod n) = 0
THM	mod_mod	x:, n:. ((x mod n) mod n) = (x mod n)