Definition: fset
fset(T) == x,y:T List//set-equal(T;x;y)
Lemma: fset_wf
∀[T:Type]. (fset(T) ∈ Type)
Lemma: fset-subtype
∀[A,B:Type]. fset(A) ⊆r fset(B) supposing A ⊆r B
Lemma: respects-equality-fset
∀[A,B:Type]. respects-equality(fset(A);fset(B)) supposing respects-equality(A;B)
Lemma: subtype_rel_fset
∀[A,B:Type]. fset(A) ⊆r fset(B) supposing A ⊆r B
Lemma: list_subtype_fset
∀[A,B:Type]. (A List) ⊆r fset(B) supposing A ⊆r B
Definition: fset_mem
x ↓∈ s == ↓∃L:T List. ((L = s ∈ fset(T)) ∧ (x ∈ L))
Lemma: fset_mem_wf
∀[T:Type]. ∀[x:T]. ∀[s:fset(T)]. (x ↓∈ s ∈ ℙ)
Definition: fset-member
a ∈ s == ↑a ∈b s
Lemma: fset-member_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[s:fset(T)]. (a ∈ s ∈ ℙ)
Lemma: fset-member_witness
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[s:fset(T)]. (a ∈ s ⇒ (Ax ∈ a ∈ s))
Lemma: sq_stable__fset-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[s:fset(T)]. SqStable(a ∈ s)
Definition: deq-fset-member
a ∈b s == a ∈b s
Lemma: deq-fset-member_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[s:fset(T)]. (a ∈b s ∈ 𝔹)
Lemma: assert-deq-fset-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[s:fset(T)]. uiff(↑a ∈b s;a ∈ s)
Lemma: strong-subtype-fset-member-type
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[s:fset(A)]. ∀[x:B]. x ∈ A supposing x ∈ s supposing strong-subtype(A;B)
Lemma: fset-subtype2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. (s ∈ fset({z:T| z ∈ s} ))
Lemma: fset-extensionality
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:fset(T)]. uiff(x = y ∈ fset(T);∀[a:T]. uiff(a ∈ x;a ∈ y))
Definition: f-subset
xs ⊆ ys == ∀a:T. a ∈ ys supposing a ∈ xs
Lemma: f-subset_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys:fset(T)]. (xs ⊆ ys ∈ ℙ)
Lemma: f-subset_antisymmetry
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys:fset(T)]. (xs = ys ∈ fset(T)) supposing (ys ⊆ xs and xs ⊆ ys)
Lemma: f-subset_weakening
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys:fset(T)]. xs ⊆ ys supposing xs = ys ∈ fset(T)
Lemma: f-subset_transitivity
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys,zs:fset(T)]. (xs ⊆ zs) supposing (ys ⊆ zs and xs ⊆ ys)
Definition: fset-union
x ⋃ y == x ⋃ y
Lemma: fset-union_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:fset(T)]. (x ⋃ y ∈ fset(T))
Lemma: decidable__fset-member
∀[T:Type]. ∀eq:EqDecider(T). ∀x:fset(T). ∀a:T. Dec(a ∈ x)
Lemma: member-fset-union
∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:fset(T). ∀a:T. (a ∈ x ⋃ y ⇐⇒ a ∈ x ∨ a ∈ y)
Lemma: fset-union-commutes
∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y:fset(A)]. (x ⋃ y = y ⋃ x ∈ fset(A))
Lemma: fset-union-associative
∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y,z:fset(A)]. (x ⋃ y ⋃ z = x ⋃ y ⋃ z ∈ fset(A))
Lemma: fset-union-idempotent
∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x:fset(A)]. (x ⋃ x = x ∈ fset(A))
Lemma: f-subset-union
∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y:fset(A)]. x ⊆ x ⋃ y
Lemma: f-union-subset
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x,y,z:fset(A)]. uiff(x ⋃ y ⊆ z;x ⊆ z ∧ y ⊆ z)
Definition: fset-list-union
fset-list-union(eq;ss) == reduce(λx,y. x ⋃ y;{};ss)
Definition: fset-singleton
{x} == [x]
Lemma: fset-singleton_wf
∀[T:Type]. ∀[x:T]. ({x} ∈ fset(T))
Lemma: member-fset-singleton
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. uiff(y ∈ {x};y = x ∈ T)
Lemma: fset-singletons-equal
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. uiff({x} = {y} ∈ fset(T);x = y ∈ T)
Definition: fset-pair
{a,b} == [a; b]
Lemma: fset-pair_wf
∀[T:Type]. ∀[a,b:T]. ({a,b} ∈ fset(T))
Lemma: fset-pair-symmetry
∀[T:Type]. ∀[a,b:T]. ({a,b} = {b,a} ∈ fset(T))
Lemma: member-fset-pair
∀[T:Type]. ∀eq:EqDecider(T). ∀x,y,z:T. uiff(z ∈ {x,y};(z = x ∈ T) ∨ (z = y ∈ T))
Lemma: fset-pair-is-union
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ({x,y} = {x} ⋃ {y} ∈ fset(T))
Lemma: f-singleton-subset
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[a:A]. ∀[x:fset(A)]. uiff({a} ⊆ x;a ∈ x)
Definition: f-union
f-union(domeq;rngeq;s;x.g[x]) ==
accumulate (with value a and list item x):
a ⋃ g[x]
over list:
s
with starting value:
[])
Lemma: f-union_wf
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[g:T ⟶ fset(A)]. ∀[s:fset(T)].
(f-union(eqt;eqa;s;x.g[x]) ∈ fset(A))
Lemma: member-f-union-aux
∀[T,A:Type].
∀eqt:EqDecider(T). ∀eqa:EqDecider(A). ∀g:T ⟶ fset(A). ∀L:T List. ∀a:A.
(a ∈ f-union(eqt;eqa;L;x.g[x]) ⇐⇒ (∃x∈L. a ∈ g[x]))
Lemma: member-f-union
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[g:T ⟶ fset(A)]. ∀[s:fset(T)]. ∀[a:A].
uiff(a ∈ f-union(eqt;eqa;s;x.g[x]);↓∃x:T. (x ∈ s ∧ a ∈ g[x]))
Definition: fset-max
fset-max(f;s) == imax-list([0 / map(f;s)])
Definition: fset-filter
{x ∈ s | P[x]} == filter(λx.P[x];s)
Lemma: fset-filter_wf
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. ({x ∈ s | P[x]} ∈ fset(T))
Lemma: fset-filter_wf2
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. ({x ∈ s | P[x]} ∈ fset({x:T| ↑P[x]} ))
Definition: fset-mapfilter
fset-mapfilter(f;P;s) == mapfilter(f;P;s)
Lemma: fset-mapfilter_wf
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[X:Type]. ∀[f:{x:T| ↑(P x)} ⟶ X]. ∀[s:fset(T)]. (fset-mapfilter(f;P;s) ∈ fset(X))
Lemma: member-fset-filter
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[x:T]. uiff(x ∈ {x ∈ s | P[x]};{x ∈ s ∧ (↑P[x])})
Lemma: member-fset-filter2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[P:{x:T| x ∈ s} ⟶ 𝔹]. ∀[x:T]. uiff(x ∈ {x ∈ s | P[x]};{x ∈ s ∧ (↑P[x])}\000C)
Lemma: member-fset-mapfilter
∀[T:Type]. ∀[eqT:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[X:Type]. ∀[eqX:EqDecider(X)]. ∀[f:{x:T| ↑(P x)} ⟶ X]. ∀[s:fset(T)].
∀[x:X].
uiff(x ∈ fset-mapfilter(f;P;s);↓∃y:T. (y ∈ s ∧ (↑(P y)) ∧ (x = (f y) ∈ X)))
Definition: fset-map
fset-map(f;s) == map(f;s)
Lemma: fset-map_wf
∀[T,X:Type]. ∀[f:T ⟶ X]. ∀[s:fset(T)]. (fset-map(f;s) ∈ fset(X))
Lemma: member-fset-map
∀[T:Type]. ∀[eqT:EqDecider(T)]. ∀[X:Type]. ∀[eqX:EqDecider(X)]. ∀[f:T ⟶ X]. ∀[s:fset(T)]. ∀[x:X].
uiff(x ∈ fset-map(f;s);↓∃y:T. (y ∈ s ∧ (x = (f y) ∈ X)))
Lemma: fset-filter-subset
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. {x ∈ s | P[x]} ⊆ s
Lemma: fset-filter-subset2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[P:{x:T| x ∈ s} ⟶ 𝔹]. {x ∈ s | P[x]} ⊆ s
Definition: fset-find
fset-find(P;s) == hd(filter(P;s))
Lemma: fset-find_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].
(fset-find(P;s) ∈ {x:T| x ∈ s ∧ (↑(P x))} ) supposing
((∀x,y:T. (x ∈ s ⇒ y ∈ s ⇒ (↑(P x)) ⇒ (↑(P y)) ⇒ (x = y ∈ T))) and
(↓∃x:T. (x ∈ s ∧ (↑(P x)))))
Definition: fset-remove
fset-remove(eq;y;s) == {x ∈ s | ¬b(eq x y)}
Lemma: fset-remove_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T]. (fset-remove(eq;x;s) ∈ fset(T))
Lemma: member-fset-remove
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x,y:T]. uiff(x ∈ fset-remove(eq;y;s);x ∈ s ∧ (¬(x = y ∈ T)))
Definition: fset-add
fset-add(eq;x;s) == {x} ⋃ s
Lemma: fset-add_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T]. (fset-add(eq;x;s) ∈ fset(T))
Lemma: member-fset-add
∀[T:Type]. ∀eq:EqDecider(T). ∀s:fset(T). ∀x,y:T. (x ∈ fset-add(eq;y;s) ⇐⇒ (x = y ∈ T) ∨ x ∈ s)
Lemma: cons-wf-fset
∀[T:Type]. ∀[s:fset(T)]. ∀[x:T]. ([x / s] ∈ fset(T))
Lemma: fset-add-remove
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T]. fset-add(eq;x;fset-remove(eq;x;s)) = s ∈ fset(T) supposing x ∈ s
Lemma: fset-add-as-cons
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T]. (fset-add(eq;x;s) = [x / s] ∈ fset(T))
Lemma: fset-add-union
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s1,s2:fset(T)]. ∀[x:T]. (fset-add(eq;x;s1) ⋃ s2 = [x / s1 ⋃ s2] ∈ fset(T))
Definition: fset-intersection
a ⋂ b == {x ∈ a | x ∈b b}
Lemma: fset-intersection_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)]. (a ⋂ b ∈ fset(T))
Lemma: member-fset-intersection
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)]. ∀[x:T]. uiff(x ∈ a ⋂ b;x ∈ a ∧ x ∈ b)
Lemma: fset-intersection-commutes
∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y:fset(A)]. (x ⋂ y = y ⋂ x ∈ fset(A))
Lemma: fset-intersection-associative
∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y,z:fset(A)]. (x ⋂ y ⋂ z = x ⋂ y ⋂ z ∈ fset(A))
Definition: fset-null
fset-null(s) == null(s)
Lemma: fset-null_wf
∀[T:Type]. ∀[s:fset(T)]. (fset-null(s) ∈ 𝔹)
Definition: empty-fset
{} == []
Lemma: empty-fset_wf
∀[T:Type]. ({} ∈ fset(T))
Lemma: member-empty-fset
∀[eq,x:Top]. (x ∈ {} ~ False)
Lemma: assert-fset-null
∀[T:Type]. ∀[s:fset(T)]. uiff(↑fset-null(s);s = {} ∈ fset(T))
Definition: fset-disjoint
fset-disjoint(eq;as;bs) == fset-null(as ⋂ bs)
Lemma: fset-disjoint_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:fset(T)]. (fset-disjoint(eq;as;bs) ∈ 𝔹)
Lemma: assert-fset-disjoint
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:fset(T)]. uiff(↑fset-disjoint(eq;as;bs);∀x:T. (¬(x ∈ as ∧ x ∈ bs)))
Lemma: fset-max_wf
∀[T:Type]. ∀[f:T ⟶ ℕ]. ∀[s:fset(T)]. (fset-max(f;s) ∈ ℕ) supposing ∀x,y:T. Dec(x = y ∈ T)
Lemma: fset-absorption1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)]. (a ⋃ a ⋂ b = a ∈ fset(T))
Lemma: fset-absorption2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)]. (a ⋂ a ⋃ b = a ∈ fset(T))
Lemma: fset-distributive
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:fset(T)]. (a ⋂ b ⋃ c = a ⋂ b ⋃ a ⋂ c ∈ fset(T))
Lemma: fset-list-union_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ss:fset(T) List]. (fset-list-union(eq;ss) ∈ fset(T))
Lemma: mem_empty_lemma
∀a,eq:Top. (a ∈ {} ~ False)
Lemma: member-fset-list-union
∀[T:Type]. ∀eq:EqDecider(T). ∀ss:fset(T) List. ∀x:T. (x ∈ fset-list-union(eq;ss) ⇐⇒ (∃s∈ss. x ∈ s))
Lemma: f-subset-empty
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:fset(T)]. (x ⊆ {} ⇐⇒ x = {} ∈ fset(T))
Lemma: empty-fset-union
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ({} ⋃ s = s ∈ fset(T))
Lemma: f-subset-singleton
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[a:A]. ∀x:fset(A). uiff(x ⊆ {a};(x = {a} ∈ fset(A)) ∨ (x = {} ∈ fset(A)))
Lemma: fset-union-empty
∀[eq,s:Top]. (s ⋃ {} ~ s)
Lemma: fset-filter-is-empty
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].
uiff({x ∈ s | P[x]} = {} ∈ fset(T);¬(∃x:T. (x ∈ s ∧ (↑P[x]))))
Lemma: decidable__squash_exists_fset
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀eq:EqDecider(T). ∀s:fset(T). ((∀x:T. Dec(P[x])) ⇒ Dec(↓∃x:T. (x ∈ s ∧ P[x])))
Definition: fset-some
fset-some(s;x.P[x]) == ¬↑fset-null({x ∈ s | P[x]})
Lemma: fset-some_wf
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. (fset-some(s;x.P[x]) ∈ ℙ)
Lemma: fset-some-iff
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. uiff(fset-some(s;x.P[x]);¬¬(∃x:T. (x ∈ s ∧ (↑P[x]))))
Lemma: fset-some-iff2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. uiff(fset-some(s;x.P[x]);¬(∀x:T. (x ∈ s ⇒ (¬↑P[x]))))
Lemma: fset-some-iff-squash
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. uiff(fset-some(s;x.P[x]);↓∃x:T. (x ∈ s ∧ (↑P[x])))
Definition: fset-all
fset-all(s;x.P[x]) == ↑fset-null({x ∈ s | ¬bP[x]})
Lemma: fset-all_wf
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. (fset-all(s;x.P[x]) ∈ ℙ)
Lemma: fset-all-iff
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. uiff(fset-all(s;x.P[x]);∀[x:T]. ↑P[x] supposing x ∈ s)
Lemma: decidable__all_fset
∀[T:Type]. ∀eq:EqDecider(T). ∀[P:T ⟶ ℙ]. ((∀x:T. Dec(P[x])) ⇒ (∀s:fset(T). Dec(∀x:T. P[x] supposing x ∈ s)))
Lemma: fset-all-filter
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. fset-all({x ∈ s | P[x]};x.P[x])
Lemma: decidable__f-subset
∀[T:Type]. ∀eq:EqDecider(T). ∀xs,ys:fset(T). Dec(xs ⊆ ys)
Definition: deq-f-subset
deq-f-subset(eq) == λx,y. isl(TERMOF{decidable__f-subset:o, 1:l, 1:l} eq x y)
Lemma: deq-f-subset_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (deq-f-subset(eq) ∈ {d:fset(T) ⟶ fset(T) ⟶ 𝔹| ∀x,y:fset(T). (x ⊆ y ⇐⇒ ↑(d x y))} )
Lemma: assert-deq-f-subset
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:fset(T)]. uiff(↑(deq-f-subset(eq) x y);x ⊆ y)
Lemma: decidable__equal_fset
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀xs,ys:fset(T). Dec(xs = ys ∈ fset(T))))
Definition: deq-fset
deq-fset(eq) == λx,y. isl(TERMOF{decidable__equal_fset:o, 1:l, 1:l} eq x y)
Lemma: deq-fset_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (deq-fset(eq) ∈ EqDecider(fset(T)))
Lemma: assert-deq-fset
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:fset(T)]. uiff(↑(deq-fset(eq) x y);x = y ∈ fset(T))
Definition: f-proper-subset
xs ⊆≠ ys == xs ⊆ ys ∧ (¬(xs = ys ∈ fset(T)))
Lemma: f-proper-subset_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys:fset(T)]. (xs ⊆≠ ys ∈ ℙ)
Definition: f-proper-subset-dec
f-proper-subset-dec(eq;xs;ys) == (deq-f-subset(eq) xs ys) ∧b (¬b(deq-fset(eq) xs ys))
Lemma: f-proper-subset-dec_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys:fset(T)]. (f-proper-subset-dec(eq;xs;ys) ∈ 𝔹)
Lemma: assert-f-proper-subset-dec
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[xs,ys:fset(T)]. uiff(↑f-proper-subset-dec(eq;xs;ys);xs ⊆≠ ys)
Lemma: decidable__f-proper-subset
∀[T:Type]. ∀eq:EqDecider(T). ∀xs,ys:fset(T). Dec(xs ⊆≠ ys)
Definition: fset-contains-none-of
fset-contains-none-of(eq;s;cs) == fset-null({c ∈ cs | deq-f-subset(eq) c s})
Lemma: fset-contains-none-of_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[cs:fset(fset(T))]. (fset-contains-none-of(eq;s;cs) ∈ 𝔹)
Lemma: assert-fset-contains-none-of
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[cs:fset(fset(T))].
uiff(↑fset-contains-none-of(eq;s;cs);∀c:fset(T). (c ∈ cs ⇒ (¬c ⊆ s)))
Lemma: fset-contains-none-of-closed-downward
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[cs:fset(fset(T))].
∀x,y:fset(T). (y ⊆ x ⇒ (↑fset-contains-none-of(eq;x;cs)) ⇒ (↑fset-contains-none-of(eq;y;cs)))
Lemma: empty-fset-contains-none-of
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[cs:fset(fset(T))]. ↑fset-contains-none-of(eq;{};cs) supposing ¬{} ∈ cs
Definition: fset-contains-none
fset-contains-none(eq;s;x.Cs[x]) == fset-contains-none-of(eq;s;f-union(eq;deq-fset(eq);s;x.Cs[x]))
Lemma: fset-contains-none_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[Cs:T ⟶ fset(fset(T))]. (fset-contains-none(eq;s;x.Cs[x]) ∈ 𝔹)
Lemma: assert-fset-contains-none
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[Cs:T ⟶ fset(fset(T))].
uiff(↑fset-contains-none(eq;s;x.Cs[x]);∀x:T. (x ∈ s ⇒ (∀c:fset(T). (c ∈ Cs[x] ⇒ (¬c ⊆ s)))))
Lemma: empty-fset-contains-none
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. (↑fset-contains-none(eq;{};x.Cs[x]))
Lemma: fset-contains-none-closed-downward
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
∀x,y:fset(T). (y ⊆ x ⇒ (↑fset-contains-none(eq;x;a.Cs[a])) ⇒ (↑fset-contains-none(eq;y;a.Cs[a])))
Definition: fset-pairwise
fset-pairwise(x,y.R[x; y];s) == fset-null({x ∈ s | ¬bfset-null({y ∈ s | ¬bR[x; y]})})
Lemma: fset-pairwise_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. (fset-pairwise(x,y.R[x;y];s) ∈ 𝔹)
Lemma: assert-fset-pairwise
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)].
uiff(↑fset-pairwise(x,y.R[x;y];s);∀x,y:T. (↑R[x;y]) supposing (x ∈ s and y ∈ s))
Definition: fset-antichain
fset-antichain(eq;ac) == fset-pairwise(xs,ys.¬bf-proper-subset-dec(eq;xs;ys);ac)
Lemma: fset-antichain_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac:fset(fset(T))]. (fset-antichain(eq;ac) ∈ 𝔹)
Lemma: assert-fset-antichain
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac:fset(fset(T))].
uiff(↑fset-antichain(eq;ac);∀xs,ys:fset(T). (¬xs ⊆≠ ys) supposing (xs ∈ ac and ys ∈ ac))
Lemma: fset-antichain-singleton
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. (↑fset-antichain(eq;{s}))
Lemma: fset-antichain-add
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(fset(T))]. ∀[x:fset(T)].
uiff(↑fset-antichain(eq;fset-add(deq-fset(eq);x;s));(↑fset-antichain(eq;s))
∧ (∀xs:fset(T). (¬xs ⊆≠ x) ∧ (¬x ⊆≠ xs) supposing xs ∈ s))
Definition: ac-covers
ac-covers(eq;ac;x) == ¬bfset-null({y ∈ ac | deq-f-subset(eq) y x})
Lemma: ac-covers_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac:fset(fset(T))]. ∀[x:fset(T)]. (ac-covers(eq;ac;x) ∈ 𝔹)
Lemma: assert-ac-covers
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac:fset(fset(T))]. ∀[x:fset(T)].
uiff(↑ac-covers(eq;ac;x);↓∃y:fset(T). (y ∈ ac ∧ y ⊆ x))
Definition: fset-ac-le
fset-ac-le(eq;ac1;ac2) == fset-all(ac1;x.¬bfset-null({y ∈ ac2 | deq-f-subset(eq) y x}))
Lemma: fset-ac-le_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:fset(fset(T))]. (fset-ac-le(eq;ac1;ac2) ∈ ℙ)
Lemma: empty-fset-ac-le
∀[eq,a:Top]. (fset-ac-le(eq;{};a) ~ True)
Lemma: fset-ac-le-singleton-empty
∀[T:Type]. ∀eq:EqDecider(T). ∀a:fset(fset(T)). fset-ac-le(eq;a;{{}})
Lemma: fset-ac-le-iff
∀[T:Type]
∀eq:EqDecider(T). ∀ac1,ac2:fset(fset(T)).
(fset-ac-le(eq;ac1;ac2) ⇐⇒ ∀[a:fset(T)]. ↓∃b:fset(T). (b ∈ ac2 ∧ b ⊆ a) supposing a ∈ ac1)
Lemma: fset-ac-le-implies
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:fset(fset(T))].
(fset-ac-le(eq;ac1;ac2) ⇒ {∀a:fset(T). (a ∈ ac1 ⇒ (¬({y ∈ ac2 | deq-f-subset(eq) y a} = {} ∈ fset(fset(T)))))})
Lemma: fset-ac-le-implies2
∀[T:Type]
∀eq:EqDecider(T). ∀ac1,ac2:fset(fset(T)).
(fset-ac-le(eq;ac1;ac2) ⇒ {∀a:fset(T). (a ∈ ac1 ⇒ (↓∃b:fset(T). (b ∈ ac2 ∧ b ⊆ a)))})
Lemma: fset-ac-le_transitivity
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2,ac3:fset(fset(T))].
(fset-ac-le(eq;ac1;ac3)) supposing (fset-ac-le(eq;ac1;ac2) and fset-ac-le(eq;ac2;ac3))
Lemma: fset-ac-le_weakening_f-subset
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(fset(T))]. fset-ac-le(eq;a;b) supposing a ⊆ b
Lemma: fset-ac-le_weakening
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(fset(T))]. fset-ac-le(eq;a;b) supposing a = b ∈ fset(fset(T))
Lemma: fset-ac-order
∀[T:Type]. ∀eq:EqDecider(T). Order({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
Lemma: fset-max_property
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f:T ⟶ ℕ]. ∀[s:fset(T)].
((∀[x:T]. (f x) ≤ fset-max(f;s) supposing x ∈ s)
∧ (¬((∀x:T. (x ∈ s ⇒ f x < fset-max(f;s))) ∧ (¬(s = {} ∈ fset(T))))))
Definition: fset-image
f"(s) == f-union(domeq;rngeq;s;x.{f x})
Lemma: fset-image_wf
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[s:fset(T)]. (f"(s) ∈ fset(A))
Lemma: fset-image-singleton
∀[eqt,eqa,f,x:Top]. (f"({x}) ~ {f x})
Lemma: fset-image-empty
∀[eqt,eqa,f:Top]. (f"({}) ~ {})
Lemma: member-fset-image-iff
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[s:fset(T)]. ∀[a:A].
uiff(a ∈ f"(s);↓∃x:T. (x ∈ s ∧ (a = (f x) ∈ A)))
Lemma: member-fset-image
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[s:fset(T)]. ∀[x:T]. f x ∈ f"(s) supposing x ∈ s
Lemma: fset-image-union
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[x,y:fset(T)].
(f"(x ⋃ y) = f"(x) ⋃ f"(y) ∈ fset(A))
Lemma: fset-image-add
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[x:T]. ∀[s:fset(T)].
(f"(fset-add(eqt;x;s)) = {f x} ⋃ f"(s) ∈ fset(A))
Lemma: fset-image_functionality_wrt_subset
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[s1,s2:fset(T)]. f"(s1) ⊆ f"(s2) supposing s1 ⊆ s2
Lemma: fset-image-compose
∀[T,A,B:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[eqb:EqDecider(B)]. ∀[f:T ⟶ A]. ∀[g:A ⟶ B]. ∀[s:fset(T)].
(g"(f"(s)) = g o f"(s) ∈ fset(B))
Definition: fset-constrained-image
f"(s) s.t. P == f-union(domeq;rngeq;s;x.if P (f x) then {f x} else {} fi )
Lemma: fset-constrained-image_wf
∀[T,A:Type]. ∀[domeq:EqDecider(T)]. ∀[rngeq:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[s:fset(T)].
(f"(s) s.t. P ∈ fset(A))
Lemma: fset-constrained-image-singleton
∀[eqt,eqa:Top]. ∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[x:T]. (f"({x}) s.t. P ~ if P (f x) then {f x} else {} fi )
Lemma: member-fset-constrained-image-iff
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[s:fset(T)]. ∀[a:A].
uiff(a ∈ f"(s) s.t. P;↓∃x:T. (x ∈ s ∧ (a = (f x) ∈ A) ∧ (↑(P a))))
Lemma: fset-constrained-image-union
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[x,y:fset(T)].
(f"(x ⋃ y) s.t. P = f"(x) s.t. P ⋃ f"(y) s.t. P ∈ fset(A))
Lemma: fset-constrained-image_functionality_wrt_subset
∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[s1,s2:fset(T)].
f"(s1) s.t. P ⊆ f"(s2) s.t. P supposing s1 ⊆ s2
Definition: fset-closed
(s closed under fs) == (∀f∈fs.∀x:T. f x ∈ s supposing x ∈ s)
Lemma: fset-closed_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[fs:(T ⟶ T) List]. ∀[s:fset(T)]. ((s closed under fs) ∈ ℙ)
Lemma: decidable__fset-closed
∀[T:Type]. ∀eq:EqDecider(T). ∀fs:(T ⟶ T) List. ∀s:fset(T). Dec((s closed under fs))
Lemma: empty-fset-closed
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[fs:(T ⟶ T) List]. ({} closed under fs)
Lemma: fset-union-closed
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[fs:(T ⟶ T) List]. ∀[as,bs:fset(T)].
((as ⋃ bs closed under fs)) supposing ((bs closed under fs) and (as closed under fs))
Definition: fset-closure
(c = fs closure of s) == s ⊆ c ∧ (c closed under fs) ∧ (∀c':fset(T). (s ⊆ c' ⇒ (c' closed under fs) ⇒ c ⊆ c'))
Lemma: fset-closure_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[fs:(T ⟶ T) List]. ∀[s,c:fset(T)]. ((c = fs closure of s) ∈ ℙ)
Lemma: fset-closure-exists
∀[T:Type]
∀eq:EqDecider(T). ∀r:T ⟶ ℕ. ∀fs:(T ⟶ T) List.
∀s:fset(T). ∃c:fset(T). (c = fs closure of s) supposing (∀f∈fs.∀x:T. ((¬((f x) = x ∈ T)) ⇒ r (f x) < r x))
Lemma: fset-closure-exists2
∀[T:Type]
∀eq:EqDecider(T). ∀r:T ⟶ ℕ. ∀fs:{f:T ⟶ T| ∀x:T. r (f x) < r x supposing ¬((f x) = x ∈ T)} List. ∀s:fset(T).
∃c:fset(T). (c = fs closure of s)
Lemma: fset-closure-unique
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[r:T ⟶ ℕ]. ∀[fs:(T ⟶ T) List]. ∀[s,c1,c2:fset(T)].
(c1 = c2 ∈ fset(T)) supposing ((c2 = fs closure of s) and (c1 = fs closure of s))
Definition: fset-size
||s|| == ||remove-repeats(eq;s)||
Lemma: fset-size_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. (||s|| ∈ ℕ)
Lemma: fset-size-empty
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. uiff(||s|| ≤ 0;s = {} ∈ fset(T))
Lemma: fsize_empty_lemma
∀eq:Top. (||{}|| ~ 0)
Lemma: union_empty_lemma
∀b,eq:Top. (b ⋃ {} ~ b)
Lemma: empty_intersect_lemma
∀b,eq:Top. ({} ⋂ b ~ {})
Lemma: fset-size-remove
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T]. ||fset-remove(eq;x;s)|| = (||s|| - 1) ∈ ℤ supposing x ∈ s
Lemma: fset-size-add
∀[T:Type]
∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T]. ||fset-add(eq;x;s)|| = (||s|| + 1) ∈ ℤ supposing ¬x ∈ s
supposing valueall-type(T)
Lemma: fset-size-proper-subset
∀[T:Type]. ∀eq:EqDecider(T). ∀x,ys:fset(T). (ys ⊆≠ x ⇒ ||ys|| < ||x||)
Lemma: f-proper-subset_transitivity
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs,cs:fset(T). (as ⊆≠ bs ⇒ bs ⊆≠ cs ⇒ as ⊆≠ cs)
Lemma: fset-induction
∀[T:Type]
∀eq:EqDecider(T)
∀[P:fset(T) ⟶ ℙ]
((∀s:fset(T). SqStable(P[s]))
⇒ P[{}]
⇒ (∀s:fset(T). ∀x:T. (P[s] ⇒ P[fset-add(eq;x;s)] supposing ¬x ∈ s))
⇒ {∀s:fset(T). P[s]})
Lemma: fset-size-union
∀[T:Type]
∀[eq:EqDecider(T)]. ∀[a,b:fset(T)]. (||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ) supposing valueall-type(T)
Lemma: fset-to-list
∀[T:Type]
∀eq:EqDecider(T)
∀[R:T ⟶ T ⟶ ℙ]
((∀a,b:T. Dec(R a b)) ⇒ Linorder(T;a,b.R a b) ⇒ (∀s:fset(T). ∃L:T List. ∀x:T. (x ∈ s ⇐⇒ (x ∈ L))))
Definition: fset-item
item(s) == hd(s)
Lemma: fset-item_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. item(s) ∈ T supposing ||s|| = 1 ∈ ℤ
Lemma: fset-item-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. item(s) ∈ s supposing ||s|| = 1 ∈ ℤ
Lemma: fset-size-one
∀[T:Type]. ∀eq:EqDecider(T). ∀s:fset(T). (||s|| = 1 ∈ ℤ ⇐⇒ ∃x:T. (x ∈ s ∧ (∀y:T. y = x ∈ T supposing y ∈ s)))
Definition: fset-only
only x ∈ s s.t. P[x] == item({x ∈ s | P[x]})
Lemma: fset-only_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].
(only x ∈ s s.t. P[x] ∈ {x:T| x ∈ s ∧ (↑P[x])} ) supposing
((∀x,y:T. (x ∈ s ⇒ y ∈ s ⇒ (↑P[x]) ⇒ (↑P[y]) ⇒ (x = y ∈ T))) and
(¬(∀x:T. (x ∈ s ⇒ (¬↑P[x])))))
Definition: up-set
up-set(T;eq;x,y.le[x; y];s) == ∀x,y:T. (x ∈ s ⇒ le[x; y] ⇒ y ∈ s)
Lemma: up-set_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[le:T ⟶ T ⟶ ℙ]. ∀[s:fset(T)]. (up-set(T;eq;x,y.le[x;y];s) ∈ ℙ)
Definition: fset-minimal
fset-minimal(x,y.less[x; y];s;a) == fset-null({y ∈ s | less[y; a]})
Lemma: fset-minimal_wf
∀[T:Type]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[a:T]. (fset-minimal(x,y.less[x;y];s;a) ∈ 𝔹)
Lemma: assert-fset-minimal
∀[T:Type]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[a:T]. uiff(↑fset-minimal(x,y.less[x;y];s;a);fset-all(s;y.¬bless[y;a]))
Definition: fset-minimals
fset-minimals(x,y.less[x; y]; s) == {a ∈ s | fset-minimal(x,y.less[x; y];s;a)}
Lemma: fset-minimals_wf
∀[T:Type]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. (fset-minimals(x,y.less[x;y]; s) ∈ fset(T))
Lemma: member-fset-minimals
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[a:T].
uiff(a ∈ fset-minimals(x,y.less[x;y]; s);a ∈ s ∧ fset-all(s;y.¬bless[y;a]))
Lemma: filter-fset-minimals
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[P:T ⟶ 𝔹].
{a ∈ fset-minimals(x,y.less[x;y]; s) | P[a]} = fset-minimals(x,y.less[x;y]; {a ∈ s | P[a]}) ∈ fset(T)
supposing ∀a,y:T. ((↑P[a]) ⇒ (↑less[y;a]) ⇒ (↑P[y]))
Lemma: implies-member-fset-minimals
∀[T:Type]
∀eq:EqDecider(T). ∀s:fset(fset(T)). ∀a:fset(T).
(a ∈ s
⇒ (¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a)))
⇒ a ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s))
Lemma: fset-minimals-antichain
∀[T:Type]
∀eq:EqDecider(T). ∀s:fset(fset(T)). (↑fset-antichain(eq;fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s)))
Lemma: fset-minimals-singleton
∀[T:Type]
∀eq:EqDecider(T). ∀x:fset(T). (fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); {x}) = {x} ∈ fset(fset(T)))
Lemma: fset-minimals-ac-le
∀[T:Type]. ∀eq:EqDecider(T). ∀s:fset(fset(T)). fset-ac-le(eq;s;fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s))
Definition: list-powerset
list-powerset(eq;L) == reduce(λu,p. p ⋃ λs.fset-add(eq;u;s)"(p);{{}};L)
Lemma: list-powerset_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. (list-powerset(eq;L) ∈ {p:fset(fset(T))| ∀x:fset(T). (x ∈ p ⇐⇒ x ⊆ L)} )
Definition: fset-powerset
fset-powerset(eq;s) == list-powerset(eq;s)
Lemma: fset-powerset_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. (fset-powerset(eq;s) ∈ {p:fset(fset(T))| ∀x:fset(T). (x ∈ p ⇐⇒ x ⊆ s)} )
Definition: fset-ac-lub
fset-ac-lub(eq;ac1;ac2) == fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); ac1 ⋃ ac2)
Lemma: fset-ac-lub_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
(fset-ac-lub(eq;ac1;ac2) ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
Lemma: fset-ac-lub-covers
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]. ∀[a:fset(T)].
(((↑ac-covers(eq;x;a)) ∨ (↑ac-covers(eq;y;a))) ⇒ (↑ac-covers(eq;fset-ac-lub(eq;x;y);a)))
Lemma: fset-ac-lub-is-lub
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
least-upper-bound({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);
ac1;ac2;fset-ac-lub(eq;ac1;ac2))
Lemma: fset-ac-lub-is-lub-constrained
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[ac1,ac2:{ac:fset(fset(T))|
(↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ].
least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);
ac1;ac2;fset-ac-lub(eq;ac1;ac2))
Definition: fset-constrained-ac-lub
lub(P;ac1;ac2) == fset-ac-lub(eq;ac1;ac2)
Lemma: fset-constrained-ac-lub_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[ac1,ac2:{ac:fset(fset(T))|
(↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} ].
(lub(P;ac1;ac2) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} )
Lemma: fset-constrained-ac-lub-is-lub
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[ac1,ac2:{ac:fset(fset(T))|
(↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ].
least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);
ac1;ac2;lub(P;ac1;ac2))
Definition: fset-ac-glb
fset-ac-glb(eq;ac1;ac2) ==
fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); f-union(deq-fset(eq);deq-fset(eq);ac1;as.λbs.as ⋃ bs"(ac2)))
Lemma: fset-ac-glb_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
(fset-ac-glb(eq;ac1;ac2) ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
Lemma: fset-ac-glb-is-glb
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
greatest-lower-bound({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);ac1;ac2;fset-ac-glb(eq\000C;ac1;ac2))
Lemma: fset-ac-le-distributive
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
(fset-ac-glb(eq;a;fset-ac-lub(eq;b;c))
= fset-ac-lub(eq;fset-ac-glb(eq;a;b);fset-ac-glb(eq;a;c))
∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
Definition: fset-constrained-ac-glb
glb(P;ac1;ac2) ==
fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); f-union(deq-fset(eq);deq-fset(eq);ac1;as.λbs.as ⋃ bs"(ac2) s.t. P))
Lemma: fset-constrained-ac-glb_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[ac1,ac2:fset(fset(T))].
(glb(P;ac1;ac2) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} )
Lemma: fset-constrained-ac-glb-is-glb
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹].
∀[ac1,ac2:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ].
greatest-lower-bound({ac:fset(fset(T))|
(↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);ac1;ac2;glb(P;\000Cac1;ac2))
supposing ∀x,y:fset(T). (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
Lemma: fset-ac-order-constrained
∀[T:Type]
∀eq:EqDecider(T). ∀P:fset(T) ⟶ 𝔹.
Order({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
Lemma: fset-ac-le-distributive-constrained
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹].
∀[a,b,c:{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ].
(glb(P;a;lub(P;b;c))
= lub(P;glb(P;a;b);glb(P;a;c))
∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} )
supposing ∀x,y:fset(T). (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
Home
Index