---

Step * 1 1 1 1 1 1 1 1 1 1 2 1 2 2 1 2 1 2 1 of Lemma one-dimensional-dM

.....equality..... 
1. i : ℕ
2. ∀[x,y:fset(fset(names({i}) + names({i})))].
     uiff(↑(deq-fset(deq-fset(union-deq(names({i});names({i});NamesDeq;NamesDeq))) x y);x
     = y
     ∈ fset(fset(names({i}) + names({i}))))
3. ∀x,y:fset(fset(names({i}) + names({i}))).  Dec(x = y ∈ fset(fset(names({i}) + names({i}))))
4. v : fset(fset(names({i}) + names({i})))
5. x : fset(names({i}) + names({i}))
6. ¬x ∈ v
7. ↑fset-antichain(union-deq(names({i});names({i});NamesDeq;NamesDeq);v)
8. ∀xs:fset(names({i}) + names({i})). (¬xs ⊆≠ {inr i }) ∧ (¬{inr i } ⊆≠ xs) supposing xs ∈ v
9. x = {inr i } ∈ fset(names({i}) + names({i}))
10. ∀[x,y:fset(names({i}) + names({i}))].
      uiff(↑(deq-fset(union-deq(names({i});names({i});NamesDeq;NamesDeq)) x y);x = y ∈ fset(names({i}) + names({i})))
11. ∀x,y:fset(names({i}) + names({i})).  Dec(x = y ∈ fset(names({i}) + names({i})))
12. v = {{inl i}} ∈ fset(fset(names({i}) + names({i})))
⊢ fset-add(deq-fset(union-deq(names({i});names({i});NamesDeq;NamesDeq));{inr i };{{inl i}}) ~ {{inl i},{inr i }}
BY
{ RepeatFor 3 ((RepeatFor 2 (Computation) THEN EqCD THEN Try (Trivial))) }

---

Latex:

---

Latex:
.....equality..... 
1.  i  :  \mBbbN{}
2.  \mforall{}[x,y:fset(fset(names(\{i\})  +  names(\{i\})))].
          uiff(\muparrow{}(deq-fset(deq-fset(union-deq(names(\{i\});names(\{i\});NamesDeq;NamesDeq)))  x  y);x  =  y)
3.  \mforall{}x,y:fset(fset(names(\{i\})  +  names(\{i\}))).    Dec(x  =  y)
4.  v  :  fset(fset(names(\{i\})  +  names(\{i\})))
5.  x  :  fset(names(\{i\})  +  names(\{i\}))
6.  \mneg{}x  \mmember{}  v
7.  \muparrow{}fset-antichain(union-deq(names(\{i\});names(\{i\});NamesDeq;NamesDeq);v)
8.  \mforall{}xs:fset(names(\{i\})  +  names(\{i\})).  (\mneg{}xs  \msubseteq{}\mneq{}  \{inr  i  \})  \mwedge{}  (\mneg{}\{inr  i  \}  \msubseteq{}\mneq{}  xs)  supposing  xs  \mmember{}  v
9.  x  =  \{inr  i  \}
10.  \mforall{}[x,y:fset(names(\{i\})  +  names(\{i\}))].
            uiff(\muparrow{}(deq-fset(union-deq(names(\{i\});names(\{i\});NamesDeq;NamesDeq))  x  y);x  =  y)
11.  \mforall{}x,y:fset(names(\{i\})  +  names(\{i\})).    Dec(x  =  y)
12.  v  =  \{\{inl  i\}\}
\mvdash{}  fset-add(deq-fset(union-deq(names(\{i\});names(\{i\});NamesDeq;NamesDeq));\{inr  i  \};\{\{inl  i\}\}) 
\msim{}  \{\{inl  i\},\{inr  i  \}\}


By

---

Latex:
RepeatFor  3  ((RepeatFor  2  (Computation)  THEN  EqCD  THEN  Try  (Trivial)))

---

Home Index