Step
*
2
1
2
1
1
1
of Lemma
list-powerset_wf
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. p : fset(fset(T))
6. ∀x:fset(T). (x ∈ p
⇐⇒ x ⊆ v)
7. x : fset(T)
8. x ⊆ v ∨ (↓∃x1:fset(T). (x1 ⊆ v ∧ (x = fset-add(eq;u;x1) ∈ fset(T))))
⊢ x ⊆ [u / v]
BY
{ D -1 }
1
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. p : fset(fset(T))
6. ∀x:fset(T). (x ∈ p
⇐⇒ x ⊆ v)
7. x : fset(T)
8. x ⊆ v
⊢ x ⊆ [u / v]
2
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. p : fset(fset(T))
6. ∀x:fset(T). (x ∈ p
⇐⇒ x ⊆ v)
7. x : fset(T)
8. ↓∃x1:fset(T). (x1 ⊆ v ∧ (x = fset-add(eq;u;x1) ∈ fset(T)))
⊢ x ⊆ [u / v]
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. p : fset(fset(T))
6. \mforall{}x:fset(T). (x \mmember{} p \mLeftarrow{}{}\mRightarrow{} x \msubseteq{} v)
7. x : fset(T)
8. x \msubseteq{} v \mvee{} (\mdownarrow{}\mexists{}x1:fset(T). (x1 \msubseteq{} v \mwedge{} (x = fset-add(eq;u;x1))))
\mvdash{} x \msubseteq{} [u / v]
By
Latex:
D -1
Home
Index