Step
*
1
of Lemma
constrained-antichain-lattice_wf
.....wf.....
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T). (y ⊆ x
⇒ (↑(P x))
⇒ (↑(P y)))
5. ↑(P {})
⊢ {{}} ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)}
BY
{ ((Assert {{}} ∈ fset(fset(T)) BY
Auto)
THEN MemTypeCD
THEN Auto
THEN (InstLemma `fset-all-iff` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
THEN BHyp -1
THEN Auto
THEN (RWO "member-fset-singleton" (-1) THENA Auto)) }
1
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T). (y ⊆ x
⇒ (↑(P x))
⇒ (↑(P y)))
5. ↑(P {})
6. {{}} ∈ fset(fset(T))
7. ↑fset-antichain(eq;{{}})
8. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
9. x : fset(T)
10. x = {} ∈ fset(T)
⊢ ↑(P x)
Latex:
Latex:
.....wf.....
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) {}\mrightarrow{} \mBbbB{}
4. \mforall{}x,y:fset(T). (y \msubseteq{} x {}\mRightarrow{} (\muparrow{}(P x)) {}\mRightarrow{} (\muparrow{}(P y)))
5. \muparrow{}(P \{\})
\mvdash{} \{\{\}\} \mmember{} \{ac:fset(fset(T))| (\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;x.P x)\}
By
Latex:
((Assert \{\{\}\} \mmember{} fset(fset(T)) BY
Auto)
THEN MemTypeCD
THEN Auto
THEN (InstLemma `fset-all-iff` [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{} THENA Auto)
THEN BHyp -1
THEN Auto
THEN (RWO "member-fset-singleton" (-1) THENA Auto))
Home
Index