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) ⊆fset(B) supposing A ⊆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) ⊆fset(B) supposing A ⊆B

Lemma: list_subtype_fset
[A,B:Type].  (A List) ⊆fset(B) supposing A ⊆B

Definition: fset_mem
x ↓∈ ==  ↓∃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 ∈ ==  ↑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 ∈  (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 ==  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 ∈ supposing x ∈ 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 ⋃ ==  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 ⋃ ⇐⇒ a ∈ x ∨ a ∈ y)

Lemma: fset-union-commutes
[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y:fset(A)].  (x ⋃ y ⋃ x ∈ fset(A))

Lemma: fset-union-associative
[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y,z:fset(A)].  (x ⋃ y ⋃ x ⋃ y ⋃ z ∈ fset(A))

Lemma: fset-union-idempotent
[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x:fset(A)].  (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 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 ∈ P[x]} ==  filter(λx.P[x];s)

Lemma: fset-filter_wf
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].  ({x ∈ P[x]} ∈ fset(T))

Lemma: fset-filter_wf2
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].  ({x ∈ 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 ∈ 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 ∈ 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 ∈ P[x]} ⊆ s

Lemma: fset-filter-subset2
[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[P:{x:T| x ∈ s}  ⟶ 𝔹].  {x ∈ 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 ∈  y ∈  (↑(P x))  (↑(P y))  (x y ∈ T))) and 
     (↓∃x:T. (x ∈ s ∧ (↑(P x)))))

Definition: fset-remove
fset-remove(eq;y;s) ==  {x ∈ | ¬b(eq 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 ⋂ ==  {x ∈ 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 ⋂ x ∈ fset(A))

Lemma: fset-intersection-associative
[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y,z:fset(A)].  (x ⋂ y ⋂ 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 ⋂ a ∈ fset(T))

Lemma: fset-absorption2
[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)].  (a ⋂ a ⋃ a ∈ fset(T))

Lemma: fset-distributive
[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:fset(T)].  (a ⋂ b ⋃ 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 ⊆ {} ⇐⇒ {} ∈ fset(T))

Lemma: empty-fset-union
[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  ({} ⋃ 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 ∈ 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 ∈ 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 ∈  (¬↑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 ∈ | ¬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 ∈ 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 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 ⊆ ⇐⇒ ↑(d y))} )

Lemma: assert-deq-f-subset
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:fset(T)].  uiff(↑(deq-f-subset(eq) 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 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) 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) 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 ⊆  (↑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 ∈  (∀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 ⊆  (↑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 ∈ | ¬bfset-null({y ∈ | ¬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 ∈ 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) 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) 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) 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 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 ∈  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].  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)) f"(s) ∈ fset(B))

Definition: fset-constrained-image
f"(s) s.t. ==  f-union(domeq;rngeq;s;x.if (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. if (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. 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. supposing s1 ⊆ s2

Definition: fset-closed
(s closed under fs) ==  (∀f∈fs.∀x:T. x ∈ 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))  (f x) < x))

Lemma: fset-closure-exists2
[T:Type]
  ∀eq:EqDecider(T). ∀r:T ⟶ ℕ. ∀fs:{f:T ⟶ T| ∀x:T. (f 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.  ({} ⋂ {})

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 ∈ 
  supposing valueall-type(T)

Lemma: fset-size-proper-subset
[T:Type]. ∀eq:EqDecider(T). ∀x,ys:fset(T).  (ys ⊆≠  ||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 b))  Linorder(T;a,b.R b)  (∀s:fset(T). ∃L:T List. ∀x:T. (x ∈ ⇐⇒ (x ∈ L))))

Definition: fset-item
item(s) ==  hd(s)

Lemma: fset-item_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  item(s) ∈ supposing ||s|| 1 ∈ ℤ

Lemma: fset-item-member
[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  item(s) ∈ supposing ||s|| 1 ∈ ℤ

Lemma: fset-size-one
[T:Type]. ∀eq:EqDecider(T). ∀s:fset(T).  (||s|| 1 ∈ ℤ ⇐⇒ ∃x:T. (x ∈ s ∧ (∀y:T. x ∈ supposing y ∈ s)))

Definition: fset-only
only x ∈ s.t. P[x] ==  item({x ∈ P[x]})

Lemma: fset-only_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].
  (only x ∈ s.t. P[x] ∈ {x:T| x ∈ s ∧ (↑P[x])} supposing 
     ((∀x,y:T.  (x ∈  y ∈  (↑P[x])  (↑P[y])  (x y ∈ T))) and 
     (∀x:T. (x ∈  (¬↑P[x])))))

Definition: up-set
up-set(T;eq;x,y.le[x; y];s) ==  ∀x,y:T.  (x ∈  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 ∈ 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 ∈ 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 ∈ 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 ∈ ⇐⇒ 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 ∈ ⇐⇒ 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 ⊆  (↑(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 ⊆  (↑(P x))  (↑(P y)))



Home Index