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