Lemma: no-repeats-iff-count
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].
uiff(no_repeats(T;L);∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ))
Lemma: sq-decider-list-deq
∀[eq:Base]. sq-decider(list-deq(eq)) supposing sq-decider(eq)
Lemma: deq-member-firstn
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L:A List]. ∀[n:ℕ+].
∀[x:A]. (x ∈b firstn(n;L) ~ x ∈b firstn(n - 1;L) ∨b(eqof(eq) x L[n - 1])) supposing n - 1 < ||L||
Lemma: deq-member-length-filter
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L:A List]. ∀[x:A]. (x ∈b L ~ 0 <z ||filter(λy.(eq y x);L)||)
Lemma: deq-member-length-filter2
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L:A List]. ∀[x:A]. (x ∈b L ~ 0 <z ||filter(λy.(eq x y);L)||)
Lemma: l_member-iff-length-filter
∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀x:A. (1 ≤ ||filter(eq x;L)|| ⇐⇒ (x ∈ L))
Lemma: apply-alist-no_repeats
∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[L:(T × A) List].
∀[x:T]. ∀[a:A]. apply-alist(eq;L;x) = (inl a) ∈ (A?) supposing (<x, a> ∈ L)
supposing no_repeats(T;map(λp.(fst(p));L))
Lemma: no_repeats-update-alist
∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[a:A]. ∀[f:A ⟶ A]. ∀[L:(T × A) List].
no_repeats(T;map(λp.(fst(p));update-alist(eq;L;x;a;n.f[n]))) supposing no_repeats(T;map(λp.(fst(p));L))
Lemma: mapfilter-no-rep-fun
∀[T,U,V:Type]. ∀[eq:EqDecider(U)]. ∀[L:T List]. ∀[u:U]. ∀[f:T ⟶ U]. ∀[g:{x:{x:T| (x ∈ L)} | ↑(eq f[x] u)} ⟶ V].
||mapfilter(g;λx.(eq f[x] u);L)|| ≤ 1 supposing no_repeats(U;map(f;L))
Definition: possible-majority
possible-majority(T;eq;L;x) == ∀y:T. (||L|| < 2 * count(eq y;L) ⇒ (y = x ∈ T))
Lemma: possible-majority_wf
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T. (possible-majority(T;eq;L;x) ∈ ℙ)
Definition: poss-maj
poss-maj(eq;L;x) ==
accumulate (with value p and list item z):
let n,x = p
in if eq z x then <n + 1, x>
if (n =z 0) then <1, z>
else <n - 1, x>
fi
over list:
L
with starting value:
<0, x>)
Lemma: poss-maj_wf
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T. (poss-maj(eq;L;x) ∈ ℕ × T)
Lemma: poss-maj-invariant
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T.
let n,z = poss-maj(eq;L;x)
in ((count(eq z;L) - count(λt.(¬b(eq z t));L)) ≤ n)
∧ (∀y:T. ((¬↑(eq z y)) ⇒ (n ≤ (count(λt.(¬b(eq y t));L) - count(eq y;L)))))
Lemma: poss-maj-property
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T. possible-majority(T;eq;L;snd(poss-maj(eq;L;x)))
Lemma: poss-maj-unanimous
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x,y:T. ((poss-maj(eq;L;x) = <||L||, y> ∈ (ℕ × T)) ⇒ (∀z∈L.z = y ∈ T))
Lemma: poss-maj-member
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. ∀x:T. (snd(poss-maj(eq;L;x)) ∈ [x / L])
Lemma: poss-maj-length
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. ((fst(poss-maj(eq;L;x))) ≤ ||L||)
Lemma: poss-maj-length2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. ∀[n:ℤ]. n ≤ ||L|| supposing (fst(poss-maj(eq;L;x))) = n ∈ ℤ
Lemma: map-simplify-test
∀[H,f,g:Base]. ∀[L:Atom List]. (map(λx.H[if x ∈b L then f[x] else g[x] fi ];L) ~ map(λx.H[f[x]];L))
Definition: weak-update-alist
weak-update-alist(eq;L;x;z;v.f[v]) == update-alist(eq;L;x;z;v.f[v])
Lemma: weak-update-alist_wf
∀[A,T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹]. ∀[x:T]. ∀[L:(T × A) List]. ∀[z:A]. ∀[f:A ⟶ A].
(weak-update-alist(eq;L;x;z;v.f[v]) ∈ (T × A) List)
Definition: remove-alist
remove-alist(eq;L;x) == rec-case(L) of [] => [] | p::ps => r.let a,v = p in if eq a x then r else [p / r] fi
Lemma: remove-alist_wf
∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:(T × A) List]. (remove-alist(eq;L;x) ∈ (T × A) List)
Definition: count-repeats
count-repeats(L,eq) ==
accumulate (with value cvs and list item v):
update-alist(eq;cvs;v;1;n.n + 1)
over list:
L
with starting value:
[])
Lemma: count-repeats_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (count-repeats(L,eq) ∈ (T × ℕ+) List)
Lemma: no_repeats-count-repeats1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. no_repeats(T;map(λp.(fst(p));count-repeats(L,eq)))
Lemma: apply-alist-count-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List].
(apply-alist(eq;count-repeats(L,eq);x) = if x ∈b L then inl ||filter(λy.(eq y x);L)|| else inr ⋅ fi ∈ (ℕ+?))
Lemma: member-count-repeats1
∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀L:T List. ((x ∈ map(λp.(fst(p));count-repeats(L,eq))) ⇐⇒ (x ∈ L))
Lemma: member-count-repeats2
∀[T:Type]
∀eq:EqDecider(T). ∀L:T List. ∀i:ℕ||count-repeats(L,eq)||.
let x,n = count-repeats(L,eq)[i]
in n = ||filter(λy.(eq y x);L)|| ∈ ℤ
Lemma: member-count-repeats3
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. ∀[n:ℕ+].
n = ||filter(λy.(eq y x);L)|| ∈ ℤ supposing (<x, n> ∈ count-repeats(L,eq))
Lemma: sum-count-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (Σ(snd(count-repeats(L,eq)[i]) | i < ||count-repeats(L,eq)||) = ||L|| ∈ ℤ)
Definition: strict-majority
strict-majority(eq;L) ==
let ms = filter(λp.||L|| <z 2 * (snd(p));count-repeats(L,eq)) in
if null(ms) then inr ⋅ else inl (fst(hd(ms))) fi
Lemma: strict-majority_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (strict-majority(eq;L) ∈ T?)
Lemma: strict-majority-property
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T].
uiff(||L|| < 2 * ||filter(λy.(eq y x);L)||;strict-majority(eq;L) = (inl x) ∈ (T?))
Lemma: strict-majority_functionality
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
(strict-majority(eq;L1) = strict-majority(eq;L2) ∈ (T?)) supposing
((||L1|| = ||L2|| ∈ ℤ) and
(∀x:T. (||filter(λy.(eq y x);L1)|| = ||filter(λy.(eq y x);L2)|| ∈ ℤ)))
Definition: strict-majority-or-first
strict-majority-or-first(eq;L) == case strict-majority(eq;L) of inl(x) => x | inr(z) => hd(L)
Lemma: strict-majority-or-first_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:{L:T List| ||L|| ≥ 1 } ]. (strict-majority-or-first(eq;L) ∈ T)
Definition: strict-majority-or-max
strict-majority-or-max(L) ==
case strict-majority(IntDeq;L) of inl(x) => x | inr(z) => if null(L) then 0 else imax-list(L) fi
Lemma: strict-majority-or-max_wf
∀[L:ℤ List]. (strict-majority-or-max(L) ∈ ℤ)
Lemma: strict-majority-or-max-property
∀t:ℕ. ∀L:ℤ List.
((∀v:ℤ
(strict-majority-or-max(L) = v ∈ ℤ) supposing
(((t + 1) ≤ ||filter(λx.(x =z v);L)||) and
(||L|| = ((2 * t) + 1) ∈ ℤ)))
∧ (strict-majority-or-max(L) ∈ L) supposing ||L|| ≥ 1 )
Definition: deq-disjoint
deq-disjoint(eq;as;bs) == (∀a∈as.¬ba ∈b bs)_b
Lemma: deq-disjoint_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List]. (deq-disjoint(eq;as;bs) ∈ 𝔹)
Lemma: assert-deq-disjoint
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List]. uiff(↑deq-disjoint(eq;as;bs);l_disjoint(A;as;bs))
Definition: deq-all-disjoint
deq-all-disjoint(eq;ass;bs) == (∀as∈ass.deq-disjoint(eq;as;bs))_b
Lemma: deq-all-disjoint_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[ass:A List List]. ∀[bs:A List]. (deq-all-disjoint(eq;ass;bs) ∈ 𝔹)
Lemma: assert-deq-all-disjoint
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[ass:A List List]. ∀[bs:A List].
uiff(↑deq-all-disjoint(eq;ass;bs);(∀as∈ass.l_disjoint(A;as;bs)))
Definition: discrete_struct
DS(A) == sort:A ⟶ Type × (a:A ⟶ EqDecider(sort a))
Lemma: discrete_struct_wf
∀[A:Type]. (DS(A) ∈ 𝕌')
Definition: dstype
dstype(TypeNames; d; a) == (fst(d)) a
Lemma: dstype_wf
∀[TypeNames:Type]. ∀[d:DS(TypeNames)]. ∀[a:TypeNames]. (dstype(TypeNames; d; a) ∈ Type)
Lemma: decidable__dstype_equal
∀[A:Type]. ∀a:A. ∀d:DS(A). ∀x,y:dstype(A; d; a). Dec(x = y ∈ dstype(A; d; a))
Definition: dsdeq
dsdeq(d;a) == (snd(d)) a
Lemma: dsdeq_wf
∀[A:Type]. ∀[d:DS(A)]. ∀[a:A]. (dsdeq(d;a) ∈ EqDecider(dstype(A; d; a)))
Definition: dseq
dseq(d;a) == (snd(d)) a
Lemma: dseq_wf
∀[TypeNames:Type]. ∀[d:DS(TypeNames)]. ∀[a:TypeNames].
(dseq(d;a) ∈ dstype(TypeNames; d; a) ⟶ dstype(TypeNames; d; a) ⟶ 𝔹)
Definition: eq_ds
x = y == dseq(d;a) x y
Lemma: eq_ds_wf
∀[A:Type]. ∀[d:DS(A)]. ∀[a:A]. ∀[x,y:dstype(A; d; a)]. (x = y ∈ 𝔹)
Lemma: ds_property
∀[A:Type]. ∀[d:DS(A)]. ∀[a:A]. ∀[x,y:dstype(A; d; a)]. {uiff(x = y ∈ dstype(A; d; a);↑x = y)}
Definition: l-union'
l-union'(eq; as; bs) == cbv_list_accum(L,x.if x ∈b L then L else [x / L] fi ;as;bs)
Lemma: l-union-nil
∀[eq,as:Top]. (as ⋃ [] ~ as)
Lemma: filter-union
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀P:T ⟶ 𝔹. (filter(P;as ⋃ bs) = filter(P;as) ⋃ filter(P;bs) ∈ (T List))
Lemma: l-union-subset
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. as ⋃ bs ~ as supposing bs ⊆ as
Lemma: l-union-same
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as:T List]. (as ⋃ as ~ as)
Lemma: l-union_functionality_wrt-l_contains
∀[T:Type]. ∀eq:EqDecider(T). ∀as1,bs1,as2,bs2:T List. (bs1 ⊆ bs2 ⇒ as1 ⊆ as2 ⇒ as1 ⋃ bs1 ⊆ as2 ⋃ bs2)
Lemma: l-union-contained
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs,cs:T List. (as ⋃ bs ⊆ cs ⇐⇒ as ⊆ cs ∧ bs ⊆ cs)
Lemma: l-union-left-contains
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs,cs:T List. (as ⊆ bs ⇒ as ⊆ bs ⋃ cs)
Lemma: l-union-right-contains
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs,cs:T List. (as ⊆ cs ⇒ as ⊆ bs ⋃ cs)
Lemma: map-l-union
∀[T,T':Type]. ∀[f:T ⟶ T']. ∀[eq:EqDecider(T)]. ∀[eq':EqDecider(T')]. ∀[as,bs:T List].
map(f;as ⋃ bs) ~ map(f;as) ⋃ map(f;bs) supposing Inj({x:T| (x ∈ as ⋃ bs)} ;T';f)
Lemma: map-l-union-1
∀[T:Type]. ∀[f:T ⟶ T]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List].
map(f;as ⋃ bs) ~ map(f;as) ⋃ map(f;bs) supposing Inj({x:T| (x ∈ as ⋃ bs)} ;T;f)
Lemma: deq-member-union
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. ∀[x:T]. (x ∈b as ⋃ bs ~ x ∈b as ∨bx ∈b bs)
Lemma: union-contains
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. as ⊆ as ⋃ bs
Lemma: union-contains2
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. bs ⊆ as ⋃ bs
Lemma: no_repeats_union
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. no_repeats(T;as ⋃ bs) supposing no_repeats(T;as)
Lemma: no_repeats-union-list
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ll:T List List]. no_repeats(T;l-union-list(eq;ll))
Definition: val-union
val-union(eq;as;bs) == let as ⟵ as in let bs ⟵ bs in reduce(λa,L. insert(a;L);as;bs)
Lemma: val-union_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. val-union(eq;as;bs) ∈ T List supposing valueall-type(T)
Lemma: val-union-l-union
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. val-union(eq;as;bs) ~ as ⋃ bs supposing valueall-type(T)
Definition: union-list2
union-list2(eq;ll) == rec-case(ll) of [] => [] | l1::l2 => r.if null(l2) then l1 else r ⋃ l1 fi
Lemma: union-list2_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ll:T List List]. (union-list2(eq;ll) ∈ T List)
Lemma: member-union-list2
∀[T:Type]. ∀eq:EqDecider(T). ∀ll:T List List. ∀x:T. ((x ∈ union-list2(eq;ll)) ⇐⇒ ∃l:T List. ((l ∈ ll) ∧ (x ∈ l)))
Lemma: union-list2-simplify1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ll:T List List]. ∀[L:T List].
(union-list2(eq;[L; [L / ll]]) ~ union-list2(eq;[L / ll]))
Definition: no_rel_repeats
no_rel_repeats(T;R;l) == ∀i,j:ℕ. (i < ||l|| ⇒ j < ||l|| ⇒ (¬(i = j ∈ ℕ)) ⇒ (¬(R l[i] l[j])))
Lemma: no_rel_repeats_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[l:T List]. (no_rel_repeats(T;R;l) ∈ ℙ)
Definition: list-to-set
list-to-set(eq;L) == [] ⋃ L
Lemma: list-to-set_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (list-to-set(eq;L) ∈ T List)
Lemma: list-to-set-property
∀[T:Type]
∀eq:EqDecider(T). ∀L:T List. (no_repeats(T;list-to-set(eq;L)) ∧ (∀a:T. ((a ∈ list-to-set(eq;L)) ⇐⇒ (a ∈ L))))
Lemma: member-list-to-set
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. ∀a:T. ((a ∈ list-to-set(eq;L)) ⇐⇒ (a ∈ L))
Lemma: list_to_set_nil_lemma
∀eq:Top. (list-to-set(eq;[]) ~ [])
Lemma: list-to-set-cons
∀[T:Type]
∀eq:EqDecider(T). ∀L:T List. ∀a:T.
(list-to-set(eq;[a / L]) ~ if a ∈b list-to-set(eq;L) then list-to-set(eq;L) else [a / list-to-set(eq;L)] fi )
Lemma: no-repeats-list-to-set
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. list-to-set(eq;L) ~ L supposing no_repeats(T;L)
Lemma: list-to-set-filter
∀[T:Type]. ∀eq:EqDecider(T). ∀P:T ⟶ 𝔹. ∀L:T List. (list-to-set(eq;filter(P;L)) ~ filter(P;list-to-set(eq;L)))
Definition: remove-repeats
remove-repeats(eq;L) == rec-case(L) of [] => [] | a::as => r.[a / filter(λx.(¬b(eq x a));r)]
Lemma: remove-repeats_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (remove-repeats(eq;L) ∈ T List)
Lemma: remove-repeats_property
∀[T:Type]
∀eq:EqDecider(T). ∀L:T List. (no_repeats(T;remove-repeats(eq;L)) ∧ (∀a:T. ((a ∈ remove-repeats(eq;L)) ⇐⇒ (a ∈ L))))
Lemma: set-equal-remove-repeats
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. set-equal(T;remove-repeats(eq;L);L)
Lemma: member-remove-repeats
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. ∀a:T. ((a ∈ remove-repeats(eq;L)) ⇐⇒ (a ∈ L))
Lemma: remove-repeats-set-equal
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
||remove-repeats(eq;L1)|| = ||remove-repeats(eq;L2)|| ∈ ℤ supposing set-equal(T;L1;L2)
Lemma: remove-repeats-l_contains
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List]. ||remove-repeats(eq;L1)|| ≤ ||remove-repeats(eq;L2)|| supposing L1 ⊆ L2
Lemma: remove-repeats-l_contains-iff
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. (as ⊆ bs ⇐⇒ remove-repeats(eq;as) ⊆ remove-repeats(eq;bs))
Lemma: l_all-remove-repeats
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ ℙ. ((∀x∈remove-repeats(eq;L).P[x]) ⇐⇒ (∀x∈L.P[x]))
Lemma: remove-repeats-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List]. (||remove-repeats(eq;L1 @ L2)|| = ||remove-repeats(eq;L2 @ L1)|| ∈ ℤ)
Lemma: remove-repeats-append-sq
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
(remove-repeats(eq;L1 @ L2) ~ remove-repeats(eq;L1) @ filter(λx.(¬bx ∈b L1);remove-repeats(eq;L2)))
Lemma: remove-repeats-append-one
∀[T:Type]
∀eq:EqDecider(T). ∀L:T List. ∀x:T.
((||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;L)|| ∈ ℤ)
∨ (||remove-repeats(eq;L @ [x])|| = (||remove-repeats(eq;L)|| + 1) ∈ ℤ))
Lemma: remove-repeats-append-one-member
∀[T:Type]
∀eq:EqDecider(T). ∀L:T List. ∀x:T.
(((x ∈ L) ∧ (||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;L)|| ∈ ℤ))
∨ ((¬(x ∈ L)) ∧ (||remove-repeats(eq;L @ [x])|| = (||remove-repeats(eq;L)|| + 1) ∈ ℤ)))
Lemma: remove_repeats_cons_lemma
∀v,u,eq:Top. (remove-repeats(eq;[u / v]) ~ [u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
Lemma: remove_repeats_nil_lemma
∀eq:Top. (remove-repeats(eq;[]) ~ [])
Lemma: length-remove-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
||remove-repeats(eq;L1)|| = ||remove-repeats(eq;L2)|| ∈ ℤ supposing ∀x:T. ((x ∈ L1) ⇐⇒ (x ∈ L2))
Lemma: length-remove-repeats-le
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (||remove-repeats(eq;L)|| ≤ ||L||)
Lemma: remove-repeats-filter
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].
(remove-repeats(eq;filter(P;L)) = filter(P;remove-repeats(eq;L)) ∈ (T List))
Lemma: remove-repeats-no_repeats
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. no_repeats(T;remove-repeats(eq;L))
Lemma: remove-repeats-no_repeats-true
∀T:Type. ∀eq:EqDecider(T). ∀L:T List. (no_repeats(T;remove-repeats(eq;L)) ⇐⇒ True)
Lemma: remove-repeats_functionality_wrt_permutation
∀[T:Type]
∀eq:EqDecider(T). ∀L1,L2:T List. (permutation(T;L1;L2) ⇒ permutation(T;remove-repeats(eq;L1);remove-repeats(eq;L2)))
Lemma: remove-repeats-length-one
∀T:Type. ∀eq:EqDecider(T). ∀L:T List.
(||remove-repeats(eq;L)|| = 1 ∈ ℤ ⇐⇒ ∃x:T. ((x ∈ L) ∧ (∀y:T. y = x ∈ T supposing (y ∈ L))))
Lemma: permutation-iff-count1
∀[T:Type]
∀eq:T ⟶ T ⟶ 𝔹
((∀x,y:T. (↑(eq x y) ⇐⇒ x = y ∈ T))
⇒ (∀a1,b1:T List. (∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ) ⇐⇒ permutation(T;a1;b1))))
Lemma: list-to-set_functionality_wrt_permutation
∀[T:Type]
∀eq:EqDecider(T). ∀L1,L2:T List. (permutation(T;L1;L2) ⇒ permutation(T;list-to-set(eq;L1);list-to-set(eq;L2)))
Lemma: list-to-set-is-remove-repeats
∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List. permutation(T;list-to-set(eq;L);remove-repeats(eq;L))
Definition: values-for-distinct
values-for-distinct(eq;L) == map(λa.outl(apply-alist(eq;L;a));remove-repeats(eq;map(λp.(fst(p));L)))
Lemma: values-for-distinct_wf
∀[A,V:Type]. ∀[eq:EqDecider(A)]. ∀[L:(A × V) List]. (values-for-distinct(eq;L) ∈ V List)
Lemma: values-for-distinct-property
∀[A,V:Type].
∀eq:EqDecider(A). ∀L:(A × V) List.
((||values-for-distinct(eq;L)|| = ||remove-repeats(eq;map(λp.(fst(p));L))|| ∈ ℤ)
∧ (∀i:ℕ||remove-repeats(eq;map(λp.(fst(p));L))||
(<remove-repeats(eq;map(λp.(fst(p));L))[i], values-for-distinct(eq;L)[i]> ∈ L)))
Lemma: values-for-distinct-nil
∀[A,V:Type]. ∀[eq:EqDecider(A)]. ∀[L:(A × V) List].
uiff(values-for-distinct(eq;L) = [] ∈ (V List);L = [] ∈ ((A × V) List))
Lemma: member-values-for-distinct
∀[A,V:Type].
∀eq:EqDecider(A). ∀L:(A × V) List. ∀a:A.
((a ∈ map(λp.(fst(p));L)) ⇒ (∃v:V. ((v ∈ values-for-distinct(eq;L)) ∧ (<a, v> ∈ L))))
Lemma: member-values-for-distinct2
∀[A,V:Type]. ∀eq:EqDecider(A). ∀L:(A × V) List. ∀v:V. ((v ∈ values-for-distinct(eq;L)) ⇒ (∃a:A. (<a, v> ∈ L)))
Lemma: list_accum-remove-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
(∀[as:T List]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
remove-repeats(eq;as)
with starting value:
n)
∈ A)) supposing
((∀x:A. (f[x;x] = x ∈ A)) and
Assoc(A;λx,y. f[x;y]) and
Comm(A;λx,y. f[x;y]))
Lemma: list_accum-set-equal-idemp
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
(∀[as,bs:T List].
∀[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n)
∈ A)
supposing set-equal(T;as;bs)) supposing
((∀x:A. (f[x;x] = x ∈ A)) and
Assoc(A;λx,y. f[x;y]) and
Comm(A;λx,y. f[x;y]))
Definition: remove-repeats-fun
remove-repeats-fun(eq;f;L) == rec-case(L) of [] => [] | a::as => r.[a / filter(λx.(¬b(eq (f x) (f a)));r)]
Lemma: remove-repeats-fun_wf
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List]. (remove-repeats-fun(eq;f;L) ∈ A List)
Lemma: remove-repeats-fun-nil
∀[eq,f:Top]. (remove-repeats-fun(eq;f;[]) ~ [])
Lemma: remove-repeats-fun-as-remove-repeats-map
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].
(map(f;remove-repeats-fun(eq;f;L)) = remove-repeats(eq;map(f;L)) ∈ (B List))
Lemma: remove-repeats-fun-length-as-remove-repeats-map
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].
(||remove-repeats-fun(eq;f;L)|| = ||remove-repeats(eq;map(f;L))|| ∈ ℤ)
Lemma: remove-repeats-fun-sublist
∀[A,B:Type]. ∀eq:EqDecider(B). ∀f:A ⟶ B. ∀L:A List. remove-repeats-fun(eq;f;L) ⊆ L
Lemma: remove-repeats-fun-member
∀[A,B:Type].
∀eq:EqDecider(B). ∀f:A ⟶ B. ∀L:A List. ∀a:A.
((a ∈ remove-repeats-fun(eq;f;L)) ⇐⇒ ∃i:ℕ||L||. ((L[i] = a ∈ A) ∧ (∀j:ℕi. (¬((f L[j]) = (f a) ∈ B)))))
Lemma: remove-repeats-fun-map
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].
(map(f;remove-repeats-fun(eq;f;L)) = remove-repeats(eq;map(f;L)) ∈ (B List))
Lemma: remove-repeats-fun-map2
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)} ⟶ B].
(map(f;remove-repeats-fun(eq;f;L)) = remove-repeats(eq;map(f;L)) ∈ (B List))
Lemma: remove-repeats-fun-as-filter
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[R:A ⟶ A ⟶ 𝔹]. ∀[L:A List].
(remove-repeats-fun(eq;f;L) ~ filter(λa.(¬b(∃x∈L.R[x;a] ∧b (eq (f x) (f a)))_b);L)) supposing
(sorted-by(λx,y. (↑R[x;y]);L) and
StAntiSym(A;x,y.↑R[x;y]) and
Irrefl(A;x,y.↑R[x;y]))
Lemma: remove-repeats-mapfilter-with-fun
∀[T,U:Type]. ∀[eq:EqDecider(U)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| ↑(P x)} ⟶ U].
(remove-repeats(eq;mapfilter(f;P;L))
= mapfilter(f;λa.((P a) ∧b (¬b(∃x∈L.(P x) ∧b R[x;a] ∧b (eq (f x) (f a)))_b));L)
∈ (U List)) supposing
(sorted-by(λx,y. (↑R[x;y]);L) and
StAntiSym(T;x,y.↑R[x;y]) and
Irrefl(T;x,y.↑R[x;y]))
Lemma: remove-repeats-length-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ||remove-repeats(eq;L)|| = ||L|| ∈ ℤ supposing no_repeats(T;L)
Lemma: remove-repeats-length-leq
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (||remove-repeats(eq;L)|| ≤ ||L||)
Lemma: remove-repeats-length-no-repeats-iff
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. uiff(no_repeats(T;L);||remove-repeats(eq;L)|| = ||L|| ∈ ℤ)
Definition: l_eqset
l_eqset(T;L1;L2) == ∀x:T. ((x ∈ L1) ⇐⇒ (x ∈ L2))
Lemma: l_eqset_wf
∀[T:Type]. ∀[L1,L2:T List]. (l_eqset(T;L1;L2) ∈ ℙ)
Lemma: l_contains-eq_set-no_repeats
∀[T:Type]. ∀[as,bs:T List]. ∀[eq:EqDecider(T)].
(no_repeats(T;as)) supposing (l_eqset(T;as;bs) and no_repeats(T;bs) and (||as|| = ||bs|| ∈ ℤ))
Definition: list-diff
as-bs == filter(λa.(¬ba ∈b bs);as)
Lemma: list-diff_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. (as-bs ∈ T List)
Lemma: list-diff-cons
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. ∀[x:T].
([x / as]-bs = if x ∈b bs then as-bs else [x / as-bs] fi ∈ (T List))
Lemma: list-diff-cons-single
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as:T List]. ∀[b,x:T]. [x / as]-[b] = [x / as-[b]] ∈ (T List) supposing ¬(x = b ∈ T)
Lemma: list-diff_functionality
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs,cs:T List].
as-bs = as-cs ∈ (T List) supposing ∀x:T. ((x ∈ as) ⇒ ((x ∈ bs) ⇐⇒ (x ∈ cs)))
Lemma: list-diff-property
∀[T:Type]
∀eq:EqDecider(T). ∀as,bs:T List.
((∀x:T. ((x ∈ as-bs) ⇐⇒ (x ∈ as) ∧ (¬(x ∈ bs)))) ∧ no_repeats(T;as-bs) supposing no_repeats(T;as))
Lemma: list-diff-subset
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. l_subset(T;as-bs;as)
Lemma: member-list-diff
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀x:T. ((x ∈ as-bs) ⇐⇒ (x ∈ as) ∧ (¬(x ∈ bs)))
Lemma: list-diff-diff
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs,cs:T List]. (as-bs-cs = as-bs @ cs ∈ (T List))
Lemma: list-diff2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as:T List]. ∀[b,c:T]. (as-[b; c] = as-[b]-[c] ∈ (T List))
Lemma: list-diff2-sym
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as:T List]. ∀[b,c:T]. (as-[b; c] = as-[c]-[b] ∈ (T List))
Lemma: list-diff-disjoint
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. as-bs = as ∈ (T List) supposing l_disjoint(T;as;bs)
Lemma: length-list-diff
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ((||as-bs|| ≤ ||as||) ∧ ||as-bs|| < ||as|| supposing (∃a∈as. (a ∈ bs)))
Lemma: no_repeats_list-diff
∀[T:Type]. ∀[L1,L2:T List]. ∀[eq:EqDecider(T)]. no_repeats(T;L1-L2) supposing no_repeats(T;L1)
Lemma: filter-list-diff
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List]. ∀[eq:EqDecider(T)]. (filter(P;L1-L2) ~ filter(P;L1)-filter(P;L2))
Definition: list-index
list-index(d;L;x) ==
rec-case(L) of
[] => inr ⋅
z::L' =>
r.case r of inl(n) => inl (n + 1) | inr(a) => if eqof(d) z x then inl 0 else r fi
Lemma: list-index_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List]. (list-index(eq;L;x) ∈ ℕ||L|| + Top)
Lemma: isl-list-index
∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀L:T List. (↑isl(list-index(eq;L;x)) ⇐⇒ (x ∈ L))
Lemma: list-index-property
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List]. L[outl(list-index(eq;L;x))] = x ∈ T supposing (x ∈ L)
Definition: list-index-cmp
list-index-cmp(eq;L;f) == int-minus-comparison(λx.outl(list-index(eq;L;f x)))
Lemma: list-index-cmp_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[A:Type]. ∀[f:A ⟶ T].
(list-index-cmp(eq;L;f) ∈ comparison({x:A| (f x ∈ L)} ))
Lemma: list-index-cmp-zero
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[A:Type]. ∀[f:A ⟶ T]. ∀[x,y:{x:A| (f x ∈ L)} ].
uiff((list-index-cmp(eq;L;f) x y) = 0 ∈ ℤ;(f x) = (f y) ∈ T)
Lemma: assert-exists-l_subset
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀P:(T List) ⟶ 𝔹
((∀L1,L2:T List. (set-equal(T;L1;L2) ⇒ (↑(P L1) ⇐⇒ ↑(P L2))))
⇒ (∀L:T List. (↑exists_sublist(L;P) ⇐⇒ ∃LL:T List. (l_subset(T;LL;L) ∧ (↑(P LL))))))))
Definition: round-robin
round-robin(L) == λn.L[n rem ||L||]
Lemma: round-robin_wf
∀[T:Type]. ∀[L:T List]. round-robin(L) ∈ ℕ ⟶ T supposing 0 < ||L||
Lemma: round-robin-member
∀[T:Type]. ∀L:T List. ∀n:ℕ. (round-robin(L) n ∈ L) supposing 0 < ||L||
Lemma: round-robin-onto
∀[T:Type]. ∀L:T List. (∀x∈L.∃b:ℕ. (x = (round-robin(L) b) ∈ T))
Lemma: round-robin-equal
∀[L:Top List]. ∀[b:ℕ]. (round-robin(L) (b + ||L||) ~ round-robin(L) b) supposing 0 < ||L||
Lemma: round-robin-list-index
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List]. (round-robin(L) outl(list-index(eq;L;x))) = x ∈ T supposing (x ∈ L)
Definition: ndlist
ndlist(T) == {L:T List| no_repeats(T;L)}
Lemma: ndlist_wf
∀[T:Type]. (ndlist(T) ∈ Type)
Lemma: cons-ndlist
∀[T:Type]. ∀[L:ndlist(T)]. ∀[x:T]. [x / L] ∈ ndlist(T) supposing ¬(x ∈ L)
Lemma: nil-ndlist
∀[T:Type]. ([] ∈ ndlist(T))
Definition: nd-append
L1@L2 == remove-repeats(eq;L1 @ L2)
Definition: vec
vec(T;n) == {L:T List| ||L|| = n ∈ ℤ}
Lemma: vec_wf
∀[T:Type]. ∀[n:ℕ]. (vec(T;n) ∈ Type)
Definition: vnil
vnil() == []
Lemma: vnil_wf
∀[T:Type]. (vnil() ∈ vec(T;0))
Lemma: l_member-first
∀[A:Type]. ∀d:A List. ∀x:A. ∀eq:EqDecider(A). ((x ∈ d) ⇒ (∃i:ℕ||d||. ((∀j:ℕi. (¬(d[j] = x ∈ A))) ∧ (d[i] = x ∈ A))))
Definition: retract
retract(T;f) == (∀x:T. ((f x) = x ∈ T)) ∧ (∀x:Base. ((f x)↓ ⇒ (x ∈ T)))
Lemma: retract_wf
∀[T:Type]. ∀[f:Base]. retract(T;f) ∈ ℙ supposing T ⊆r Base
Definition: retract-compose
retract-compose(h;f) == λx.eval z = h x in f x
Lemma: retract-compose_wf
∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[h:Base].
(retract-compose(h;f) ∈ {g:T ⟶ A| g = f ∈ (T ⟶ A)} ) supposing (((T ⊆r Base) ∧ (A ⊆r Base) ∧ retract(T;h)) and value\000C-type(T))
Lemma: cardinality-le-list-set
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀L:T List. |{x:T| (x ∈ L)} | ≤ ||L||))
Lemma: finite-type-list
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀L:T List. finite-type({x:T| (x ∈ L)} )))
Lemma: decidable__all-list
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀L:T List. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. ((∀x:{x:T| (x ∈ L)} . Dec(P[x])) ⇒ Dec(∀x:{x:T| (x ∈ L)} . P[x]))))
Definition: l_index
index(L;x) == mu(λi.(dT x L[i]))
Lemma: l_index_wf
∀[T:Type]. ∀[dT:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. index(L;x) ∈ ℕ||L|| supposing (x ∈ L)
Lemma: l_index_hd
∀[T:Type]. ∀[dT:EqDecider(T)]. ∀[L:T List]. index(L;hd(L)) ~ 0 supposing ¬↑null(L)
Lemma: select_l_index
∀[T:Type]. ∀[dT:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. L[index(L;x)] = x ∈ T supposing (x ∈ L)
Lemma: l_before_l_index
∀[T:Type]
∀dT:EqDecider(T). ∀L:T List. ∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ x before y ∈ L supposing index(L;x) < index(L;y))
Lemma: l_before_l_index_le
∀[T:Type]
∀dT:EqDecider(T). ∀L:T List. ∀x,y:T.
((x ∈ L) ⇒ (y ∈ L) ⇒ x before y ∈ L ∨ (x = y ∈ T) supposing index(L;x) ≤ index(L;y))
Lemma: no_repeats_mu_index
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[i:ℕ||L||]. mu(λi@0.(eq L[i] L[i@0])) = i ∈ ℤ supposing no_repeats(T;L)
Lemma: no_repeats_l_index
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[i:ℕ||L||]. index(L;L[i]) ~ i supposing no_repeats(T;L)
Lemma: no_repeats_l_index-inj
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. Inj({x:T| (x ∈ L)} ;ℕ||L||;λx.index(L;x)) supposing no_repeats(T;L)
Definition: l_intersection
(L1 ⋂ L2) == filter(λx.x ∈b L2;L1)
Lemma: l_intersection_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L1,L2:A List]. ((L1 ⋂ L2) ∈ A List)
Lemma: member-intersection
∀[A:Type]. ∀eq:EqDecider(A). ∀L1,L2:A List. ∀x:A. ((x ∈ (L1 ⋂ L2)) ⇐⇒ (x ∈ L1) ∧ (x ∈ L2))
Lemma: no_repeats-intersection
∀[A:Type]. ∀eq:EqDecider(A). ∀L1,L2:A List. (no_repeats(A;L1) ⇒ no_repeats(A;(L1 ⋂ L2)))
Lemma: l_intersection_nil
∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ((L ⋂ []) = [] ∈ (A List))
Lemma: l_disjoint_intersection
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:T List]. l_disjoint(T;(b ⋂ c);a) supposing l_disjoint(T;b;a) ∨ l_disjoint(T;c;a)
Lemma: l_disjoint_intersection2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:T List]. l_disjoint(T;a;(b ⋂ c)) supposing l_disjoint(T;a;b) ∨ l_disjoint(T;a;c)
Lemma: disjoint-iff-null-intersection
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:T List]. uiff(l_disjoint(T;a;b);(a ⋂ b) = [] ∈ (T List))
Lemma: l_disjoint_intersection_implies
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:T List]. l_disjoint(T;a;b) supposing l_disjoint(T;a;(a ⋂ b))
Lemma: l_disjoint_intersection_implies2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:T List]. l_disjoint(T;a;b) supposing l_disjoint(T;b;(a ⋂ b))
Lemma: l_intersection-size
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:T List].
(no_repeats(T;a) ⇒ no_repeats(T;b) ⇒ a ⊆ c ⇒ b ⊆ c ⇒ ((||a|| + ||b||) ≤ (||c|| + ||(a ⋂ b)||)))
Lemma: atom2-deq-aux
∀[a,b:Atom2]. uiff(a = b ∈ Atom2;↑a =a2 b)
Definition: atom2-deq
Atom2Deq == λa,b. a =a2 b
Lemma: atom2-deq_wf
Atom2Deq ∈ EqDecider(Atom2)
Definition: name
Name == Atom List
Lemma: name_wf
Name ∈ Type
Lemma: name-valueall-type
valueall-type(Name)
Definition: name-deq
NameDeq == list-deq(AtomDeq)
Lemma: name-deq_wf
NameDeq ∈ EqDecider(Name)
Lemma: sq-decider-name-deq
sq-decider(NameDeq)
Definition: name_eq
name_eq(x;y) == NameDeq x y
Lemma: name_eq_wf
∀[x,y:Name]. (name_eq(x;y) ∈ 𝔹)
Lemma: assert-name_eq
∀[x,y:Name]. uiff(↑name_eq(x;y);x = y ∈ Name)
Lemma: assert-name-deq
∀[x,y:Name]. uiff(↑(NameDeq x y);x = y ∈ Name)
Lemma: name_eq-is-inl
∀[x,y,z:Base]. x ~ y supposing name_eq(x;y) ~ inl z
Lemma: not-name_eq-implies-sq-bfalse
∀[hdr1,hdr2:Name]. name_eq(hdr1;hdr2) ~ ff supposing ¬(hdr1 = hdr2 ∈ Name)
Lemma: decidable__equal_name
∀x,y:Name. Dec(x = y ∈ Name)
Lemma: name_eq_symmetry
∀[x,y:Name]. (name_eq(x;y) ~ name_eq(y;x))
Lemma: name_eq-normalize-name
∀[X,F,G:Top]. ∀[a,b:Name].
(case name_eq(a;b) ∧b X of inl(x) => F[x;a] | inr(x) => G[x] ~ case name_eq(a;b) ∧b X
of inl(x) =>
F[x;b]
| inr(x) =>
G[x])
Lemma: name_eq_spread
∀[x,y,F:Top]. (name_eq(let a,b = x in F[a;b];y) ~ let a,b = x in name_eq(F[a;b];y))
Lemma: name_eq-normalize-name2
∀[X,F,G:Top]. ∀[a,b:Name]. (if name_eq(a;b) ∧b X then F a else G fi ~ if name_eq(a;b) ∧b X then F b else G fi )
Lemma: name_eq-normalize
∀[F,G,a,b:Top]. (if name_eq(a;b) then F a else G fi ~ if name_eq(a;b) then F b else G fi )
Lemma: name_eq-normalize2
∀[F,G,X,a,b:Top].
(case name_eq(a;b) ∧b X of inl(x) => F a | inr(y) => G ~ case name_eq(a;b) ∧b X of inl(x) => F b | inr(y) => G)
Lemma: name_eq-normalize3
∀[F,G,X,a,b:Top].
(case name_eq(a;b) ∧b X of inl(x) => F[a] | inr(y) => G ~ case name_eq(a;b) ∧b X of inl(x) => F[b] | inr(y) => G)
Lemma: name_eq-normalize4
∀[F,G,a,b:Top]. (case name_eq(a;b) of inl(x) => F a | inr(y) => G ~ case name_eq(a;b) of inl(x) => F b | inr(y) => G)
Lemma: name_eq-normalize-left
∀[F,G,a,b:Top]. (case name_eq(a;b) of inl(x) => F a | inr(y) => G ~ case name_eq(a;b) of inl(x) => F b | inr(y) => G)
Lemma: equal-by-name-cases
∀a,x,y:Name.
∀T:Type. ∀z:T. ∀P,Q:ℙ. ∀t1:⋂p:P. T. ∀t2:⋂q:Q. T.
(((a = x ∈ Name) ∧ P ∧ (z = t1 ∈ T)) ∨ ((a = y ∈ Name) ∧ Q ∧ (z = t2 ∈ T))
⇐⇒ (((a = x ∈ Name) ∧ P) ∨ ((a = y ∈ Name) ∧ Q)) ∧ (z = if name_eq(a;x) then t1 else t2 fi ∈ T))
supposing ¬(x = y ∈ Name)
Definition: name-subst
name-subst(s;x) == case apply-alist(NameDeq;s;x) of inl(z) => z | inr(z) => x
Lemma: name-subst_wf
∀[s:(Name × Name) List]. ∀[x:Name]. (name-subst(s;x) ∈ Name)
Definition: nat-to-str
nat-to-str(n) ==
fix((λnat-to-str,n. if (n =z 0) then [0]
if (n =z 1) then [1]
if (n =z 2) then [2]
if (n =z 3) then [3]
if (n =z 4) then [4]
if (n =z 5) then [5]
if (n =z 6) then [6]
if (n =z 7) then [7]
if (n =z 8) then [8]
if (n =z 9) then [9]
else (nat-to-str (n ÷ 10)) @ (nat-to-str (n rem 10))
fi ))
n
Lemma: nat-to-str_wf
∀[n:ℕ]. (nat-to-str(n) ∈ Atom List)
Lemma: member-nat-to-str
∀n:ℕ. ∀s:Atom. ((s ∈ nat-to-str(n)) ⇒ (s ∈ ``0 1 2 3 4 5 6 7 8 9``))
Definition: str1-to-nat
str1-to-nat(a) ==
if a =a "1" then 1
if a =a "2" then 2
if a =a "3" then 3
if a =a "4" then 4
if a =a "5" then 5
if a =a "6" then 6
if a =a "7" then 7
if a =a "8" then 8
if a =a "9" then 9
else 0
fi
Lemma: str1-to-nat_wf
∀[a:Atom]. (str1-to-nat(a) ∈ ℕ)
Definition: str-to-nat-plus
str-to-nat-plus(s;n) == rec-case(s) of [] => λx.x | fst::rest => rec.λx.(rec (str1-to-nat(fst) + (10 * x))) n
Lemma: str-to-nat-plus_wf
∀[s:Atom List]. ∀[n:ℕ]. (str-to-nat-plus(s;n) ∈ ℕ)
Definition: str-to-nat
str-to-nat(s) == str-to-nat-plus(s;0)
Lemma: str-to-nat_wf
∀[s:Atom List]. (str-to-nat(s) ∈ ℕ)
Lemma: str-to-nat-plus-property
∀[s:Atom List]. ∀[n:ℕ]. (str-to-nat-plus(s;n) = (str-to-nat(s) + (n * 10^||s||)) ∈ ℤ)
Lemma: str-to-nat-to-str
∀[n:ℕ]. (str-to-nat(nat-to-str(n)) = n ∈ ℤ)
Definition: mu-ge-print
mu-ge-print(f;n) ==
fix((λmu-ge,n. if f n then n else eval m = n + 1 in eval s = evalall(nat-to-str(m)) in print_line(s; mu-ge m) fi )) \000Cn
Definition: find-xover-print
find-xover-print(f;m;n;step) ==
fix((λfind-xover,m,n,step. eval s = evalall(nat-to-str(n)) in
print_line(s;
if f n
then <n, m>
else eval step' = 2 * step in
eval k = n + step in
find-xover n k step'
fi )))
m
n
step
Definition: nat-to-incomparable
nat-to-incomparable(n) == nat-to-str(n) @ [/]
Lemma: nat-to-incomparable_wf
∀[n:ℕ]. (nat-to-incomparable(n) ∈ Name)
Lemma: nat-to-incomparable-property
∀[n,m:ℕ]. ¬nat-to-incomparable(n) ≤ nat-to-incomparable(m) supposing ¬(n = m ∈ ℤ)
Definition: maybe-new
maybe-new(s;avoid) == if s ∈b avoid then let n = mu(λn.(¬bs @ nat-to-str(n) ∈b avoid)) in s @ nat-to-str(n) else s fi
Lemma: maybe-new_wf
∀[s:Name]. ∀[avoid:Name List]. (maybe-new(s;avoid) ∈ {s':Name| ¬(s' ∈ avoid)} )
Definition: Id
Id == Atom2
Lemma: Id_wf
Id ∈ Type
Lemma: Id_sq
SQType(Id)
Lemma: Id-valueall-type
valueall-type(Id)
Lemma: Id-has-valueall
∀[x:Id]. has-valueall(x)
Lemma: Id-has-value
∀[x:Id]. (x)↓
Lemma: free-from-atom-Id
∀[i:Id]. ∀[a:Atom1]. a#i:Id
Lemma: free-from-atom-Id-rw
∀[i:Id]. ∀[a:Atom1]. uiff(a#i:Id;True)
Definition: mkid
"$x" == '$x'2
Lemma: mkid-wf-test
"xxx" ∈ Id
Definition: id-deq
IdDeq == Atom2Deq
Lemma: id-deq_wf
IdDeq ∈ EqDecider(Id)
Definition: eq_id
a = b == IdDeq a b
Lemma: eq_id_wf
∀[a,b:Id]. (a = b ∈ 𝔹)
Lemma: eq_id_self
∀[a:Id]. (a = a ~ tt)
Lemma: assert-eq-id
∀[a,b:Id]. uiff(↑a = b;a = b ∈ Id)
Lemma: decidable__equal_Id
∀a,b:Id. Dec(a = b ∈ Id)
Lemma: eq_id_test
("x" = "x" ~ tt) ∧ ("x" = "y" ~ ff)
Lemma: apply-Id-alist-function
∀[x:Id]. ∀[F:Top]. ∀[L:Id List]. apply-alist(IdDeq;map(λx.<x, F[x]>;L);x) ~ inl F[x] supposing (x ∈ L)
Definition: id-graph
Graph(S) == {i:Id| (i ∈ S)} ⟶ ({i:Id| (i ∈ S)} List)
Lemma: id-graph_wf
∀[S:Id List]. (Graph(S) ∈ Type)
Definition: id-graph-edge
(i⟶j)∈G == (j ∈ G i)
Lemma: id-graph-edge_wf
∀[S:Id List]. ∀[G:Graph(S)]. ∀[i:{i:Id| (i ∈ S)} ]. ∀[j:Id]. ((i⟶j)∈G ∈ ℙ)
Lemma: id-graph-edge-implies-member
∀S:Id List. ∀G:Graph(S). ∀i:{i:Id| (i ∈ S)} . ∀j:Id. ((i⟶j)∈G ⇒ (j ∈ S))
Home
Index