Step
*
1
of Lemma
fdl-is-1_wf
1. X : Type
2. X List List ∈ Type
3. ∀as,bs:X List List. (dlattice-eq(X;as;bs) ∈ Type)
4. ∀as:X List List. dlattice-eq(X;as;as)
5. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
6. as : X List List
7. bs : X List List
8. dlattice-eq(X;as;bs)
9. 𝔹 = 𝔹 ∈ Type
⊢ fdl-is-1(as) = fdl-is-1(bs)
BY
{ (Thin (-1) THEN D -1) }
1
1. X : Type
2. X List List ∈ Type
3. ∀as,bs:X List List. (dlattice-eq(X;as;bs) ∈ Type)
4. ∀as:X List List. dlattice-eq(X;as;as)
5. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
6. as : X List List
7. bs : X List List
8. as
⇒ bs
9. bs
⇒ as
⊢ fdl-is-1(as) = fdl-is-1(bs)
Latex:
Latex:
1. X : Type
2. X List List \mmember{} Type
3. \mforall{}as,bs:X List List. (dlattice-eq(X;as;bs) \mmember{} Type)
4. \mforall{}as:X List List. dlattice-eq(X;as;as)
5. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
6. as : X List List
7. bs : X List List
8. dlattice-eq(X;as;bs)
9. \mBbbB{} = \mBbbB{}
\mvdash{} fdl-is-1(as) = fdl-is-1(bs)
By
Latex:
(Thin (-1) THEN D -1)
Home
Index