Selected Objects
| def | list_length | | | == (letrec l L = (Case of L; nil  0 ; h.t 1+l(t)) ) |
| THM | list_length_non_negative |  L:T List. ||(L) 0 |
| THM | discrete__list | Discrete{T}   Discrete{(T List)} |
| THM | null_true_lemma | L:T List. null(L) = true  L = nil |
| THM | null_false_lemma | L:T List. null(L) = false ( h:T, t:T List. L = h.t) |
| def | remove | remove(eq;x;L) == (letrec remove eq x L = (Case of L; nil nil ; h.t if eq(x,h) t else h.remove(eq,x,t) fi) ) (eq,x,L) |
| def | filter | filter(f;L) == (letrec filter f L = (Case of L; nil nil ; h.t if f(h) h.filter(f,t) else filter(f,t) fi) ) (f,L) |
| def | is_member | x( eq) L == (letrec is_member x eq L = (Case of L; nil false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L) |
| THM | sq_stable__is_member | eq:(T  T ), x:T, L:T List. SqStable(x(eq) L) |
| THM | decidable__is_member | eq:(TT), x:T, L:T List. Dec(x(eq) L) |
| THM | is_member_equalities_lemma | eq:{T=}, u:T, L:T List. u(eq) L (f:{T }. u(f) L) |
| THM | is_member_equality_strengthening_lemma | equiv:{T}, eq:{T=}, u:T, L:T List. u(equiv) L (v:T. equiv(u,v) & v(eq) L) |
| THM | hd_is_member_lemma | eq:{T}, L:T List. ||L||1 hd(L)(eq) L |
| THM | non_nil_is_member | eq:{T}, L:T List. L  nil (x:T. x(eq) L) |
| THM | is_member_cons | eq:{T}, t:T, L:T List. t(eq) (t.L) |
| def | list_all | xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L) |
| THM | list_all_tail | P:(TProp), L:T List, x:T. x(x.L).P(x) xL.P(x) |
| THM | sq_stable__list_all | P:(TProp), L:T List. (x:T. SqStable(P(x))) SqStable(xL.P(x)) |
| THM | decidable__list_all | P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x)) |
| THM | list_all_of_false_false | L:T List, x:T. x(x.L).False False |
| def | list_all_2 | xL.P(x) == (letrec all L = (Case of L; nil true ; h.t P(h) (all(t))) ) (L) |
| THM | not_list_all_2_implies_exists_not | eq:{T}, P:(T), L:T List.  xL.P(x) (x:{x:T| x(eq) L }. P(x)) |
| THM | list_all_iff_assert_list_all_2 | L:T List, P:(T). xL.P(x) xL.P(x) |
| THM | list_all_is_member_lemma | eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) |
| THM | list_all_is_member_nil_lemma | eq:(TT), L:T List. xL.x(eq) nil nil = L |
| def | list_exists | xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h)  list_exists(t)) ) (L) |
| THM | decidable__list_exists | P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x)) |
| THM | list_exists_is_member_lemma | eq:{T=}, P:(TProp), L:T List. (x:T. x(eq) L & P(x)) yL.P(y) |
| THM | list_exists_is_member_lemma1 | eq:{T=}, P:(TProp), x:T, L:T List. x(eq) L P(x) yL.P(y) |
| THM | list_exists_exists | eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x)) |
| THM | list_all_all | eq:{T=}, P:(TType), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x)) |
| THM | list_all_2_all | P:(T), L:T List. xL.P(x) xL.P(x) |
| def | list_exists_2 | xL.P(x) == (letrec exists L = (Case of L; nil false ; h.t P(h) exists(t)) ) (L) |
| THM | remove_is_member | eq:{T}, x,y:T, L:T List. x(eq) remove(eq;y;L) x(eq) L |
| THM | not_list_all_not_iff_list_exists | P:(TProp). (x:T. Dec(P(x))) (L:T List. xL.(P(x)) xL.P(x)) |
| def | disjoint | disjoint(eq;L1;L2) == xL1.x(eq) L2 |
| THM | decidable__disjoint | eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2)) |
| THM | disjoint_tail | eq:(TT), L1,L2:T List, x:T. disjoint(eq;(x.L1);L2) disjoint(eq;L1;L2) |
| def | disjoint2 | disjoint(eq;L;M) == (letrec disjoint2 L = (Case of L; nil true ; h.t if h(eq) M false else disjoint2(t) fi) ) (L) |
| THM | disjoint_iff_assert_disjoint2 | eq:{T}, L,M:T List. disjoint(eq;L;M) disjoint(eq;L;M) |
| THM | not_disjoint_is_member_lemma | eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M) |
| THM | append_nil_right_identity | L:T List. (L @ nil) = L |
| def | sublist | L1( eq)L2 == xL1.x(eq) L2 |
| THM | decidable__sublist | eq:{T}, L,M:T List. Dec(L(eq)M) |
| THM | sublist_tail | Discrete{T} (eq:{T}, u:T, v:T List. v(eq)(u.v)) |
| THM | sublist_tail1 | eq:{T=}, u:T, v:T List. v(eq)(u.v) |
| THM | sublist_list_all_lemma | EQ:{T=}, eq:{T}, L,M:T List. L(eq)M (z:T. z(EQ) L z(eq) M) |
| THM | sublist_weakening_wrt_identity | Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M) |
| THM | sublist_reflexive | eq:{T=}, L:T List. L(eq)L |
| THM | sublist_transitivity | Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(eq1)L2 L2(eq2)L3 L1(eq3)L3) |
| THM | is_member_sublist_lemma | eq:{T=}, x:T, L,M:T List. x(eq) L L(eq)M x(eq) M |
| def | sublist_2 | (eq)(L,M) == xL.x(eq) M |
| THM | sublist_iff_assert_sublist_2 | Discrete{T} (eq:{T}, L,M:T List. L(eq)M (eq)(L,M)) |
| THM | sublist_iff_assert_sublist_2_x | L,M:T List, eq:{T=}. L(eq)M (eq)(L,M) |
| THM | sublist_of_nil_iff_nil | eq:{T=}, L:T List. L(eq)nil L = nil |
| THM | append_associative | L1,L2,L3:T List. (L1 @ (L2 @ L3)) = ((L1 @ L2) @ L3) |
| THM | is_member_append_lemma | eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N))) |
| THM | is_member_append_lemma1 | eq:{T}, L:T List, x:T. x(eq) L (M,N:T List, y:T. eq(x,y) & L = (M @ (y.N))) |
| THM | is_member_of_append_lemma | eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) L x(eq) M |
| THM | is_member_append_disjunction_lemma | eq:{T}, x:T, L,M:T List. x(eq) (L @ M) x(eq) L x(eq) M |
| THM | append_commutes_under_is_member | eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) (M @ L) |
| THM | append_commutes_under_sublist | Discrete{T} (eq:{T}, L,M:T List. (L @ M)(eq)(M @ L)) |
| THM | append_commutes_under_list_iso | Discrete{T} (eq:{T}, L,M:T List. (L @ M)(~eq)(M @ L)) |
| THM | append_functionality_wrt_sublist | L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(eq1)L2 L3(eq2)L4 (L1 @ L3)(eq3)(L2 @ L4) |
| THM | append_is_member_lemma | eq:{T=}, L:T List, x:T. (M,N:T List. L = (M @ (x.N))) x(eq) L |
| THM | is_member_non_nil | eq:{T=}, u:T, L:T List. u(eq) L (v:T, M:T List. L = v.M) |
| THM | is_member_remove_lemma | eq:{T=}, L:T List, x:T. x(eq) L (M,N:T List. L = (M @ (x.N)) & remove(eq;x;L) = (M @ N)) |
| THM | is_member_tail | eq:{T}, x:T, L:T List. x(eq) L (y:T. x(eq) (y.L)) |
| THM | is_member_filter_lemma | eq:{T=}, P:(T), L:T List, x:T. x(eq) filter(( x.P(x));L) P(x) |
| THM | filter_is_member_lemma | eq:{T=}, P:(T), L:T List, x:T. x(eq) L P(x) x(eq) filter((x.P(x));L) |
| def | list_iso | L1(~eq)L2 == L1(eq)L2 & L2(eq)L1 |
| THM | list_iso_weakening_wrt_identity | Discrete{T} (eq:{T}, L,M:T List. L = M L(~eq)M) |
| THM | list_iso_commutative | eq:{T}, L,M:T List. L(~eq)M M(~eq)L |
| THM | list_iso_inversion | Discrete{T} (eq1,eq2:{T}, L,M:T List. eq1 = eq2 L(~eq1)M M(~eq2)L) |
| THM | list_iso_transitivity | Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L2(~eq2)L3 L1(~eq3)L3) |
| THM | append_functionality_wrt_list_iso | L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1 @ L3)(~eq3)(L2 @ L4) |
| THM | sublist_functionality_wrt_id_list_iso_id | L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(eq2)L3 L2(eq2)L4) |
| THM | sublist_functionality_wrt_id_id_list_iso | L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1 = L2 L3(~eq1)L4 (L1(eq2)L3 L2(eq2)L4) |
| THM | sublist_functionality_wrt_id_list_iso_list_iso | L1,L2:T List, eq1,eq2,eq3,eq4:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 eq3 = eq4 L1(~eq1)L2 L3(~eq2)L4 (L1(eq3)L3 L2(eq4)L4) |
| THM | list_iso_functionality_wrt_id_list_iso_id | L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(~eq2)L3 L2(~eq2)L4) |
| THM | list_iso_functionality_wrt_id_list_iso_list_iso | L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1(~eq3)L3 L2(~eq3)L4) |
| def | list_iso_2 | (~eq)(L,M) == ((eq)(L,M))((eq)(M,L)) |
| THM | list_iso_iff_assert_list_iso_2 | Discrete{T} (eq:{T}, L,M:T List. L(~eq)M (~eq)(L,M)) |
| THM | decidable__list_iso | eq:{T}, L,M:T List. Dec(L(~eq)M) |
| THM | decidable__equal_list | (x,y:T. Dec(x = y)) (L,M:T List. Dec(L = M)) |
| THM | not_is_member_remove_lemma | eq:{T=}, x,y:T, L:T List. x(eq) L eq(x,y) x(eq) remove(eq;y;L) |
| THM | remove_is_member_lemma | eq:{T}, u:T, L:T List, v:T. v(eq) remove(eq;u;L) v(eq) L |
| THM | list_all_append_lemma | P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) & xM.P(x) |
| THM | list_exists_append_lemma | P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x) |
| THM | list_exists_is_member_append_lemma | P:(TProp), L:T List. xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N))) |
| THM | singelton_append_equals_lemma | a:T, R,S:T List, b:T. [a] = (R @ (b.S)) a = b |
| def | is_intersection | L (eq)M == xL.x(eq) M |
| THM | is_intersection_implies_exists_element | eq:{T=}, L,M:T List. L(eq)M (x:{x:T| x(eq) L }. x(eq) M) |