---

Step * 1 of Lemma oal_merge_wf


1. a : LOSet
2. b : AbDMon
⊢ ∀ps,qs:(|a| × |b|) List.  (ps ++ qs ∈ (|a| × |b|) List)
BY
{ Assert ∀rs:(|a| × |b|) List × ((|a| × |b|) List). ((fst(rs)) ++ (snd(rs)) ∈ (|a| × |b|) List) 
THEN ((RepD) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. rs : (|a| × |b|) List × ((|a| × |b|) List)
⊢ (fst(rs)) ++ (snd(rs)) ∈ (|a| × |b|) List

2
1. a : LOSet
2. b : AbDMon
3. ∀rs:(|a| × |b|) List × ((|a| × |b|) List). ((fst(rs)) ++ (snd(rs)) ∈ (|a| × |b|) List)
4. ps : (|a| × |b|) List
5. qs : (|a| × |b|) List
⊢ ps ++ qs ∈ (|a| × |b|) List

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
\mvdash{}  \mforall{}ps,qs:(|a|  \mtimes{}  |b|)  List.    (ps  ++  qs  \mmember{}  (|a|  \mtimes{}  |b|)  List)


By

---

Latex:
Assert  \mforall{}rs:(|a|  \mtimes{}  |b|)  List  \mtimes{}  ((|a|  \mtimes{}  |b|)  List).  ((fst(rs))  ++  (snd(rs))  \mmember{}  (|a|  \mtimes{}  |b|)  List) 
THEN  ((RepD)  THENA  Auto)

---

Home Index