---

Step * 1 of Lemma assert_of_oal_null


1. s : LOSet@i'
2. g : AbDMon@i'
3. ps : |oal(s;g)|@i
⊢ ps = [] ∈ (|(s × (g↓set))| List) ⇐⇒ ps = 00 ∈ |oal(s;g)|
BY
{ ((GenRepD) THENA Auto) }

1
1. s : LOSet@i'
2. g : AbDMon@i'
3. ps : |oal(s;g)|@i
4. ps = [] ∈ (|(s × (g↓set))| List)@i
⊢ ps = 00 ∈ |oal(s;g)|

2
1. s : LOSet@i'
2. g : AbDMon@i'
3. ps : |oal(s;g)|@i
4. ps = 00 ∈ |oal(s;g)|@i
⊢ ps = [] ∈ (|(s × (g↓set))| List)

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  AbDMon@i'
3.  ps  :  |oal(s;g)|@i
\mvdash{}  ps  =  []  \mLeftarrow{}{}\mRightarrow{}  ps  =  00


By

---

Latex:
((GenRepD)  THENA  Auto)

---

Home Index