---

Step * 1 1 of Lemma oal_merge_wf


1. a : LOSet
2. b : AbDMon
3. rs : (|a| × |b|) List × ((|a| × |b|) List)
⊢ (fst(rs)) ++ (snd(rs)) ∈ (|a| × |b|) List
BY
{ ((D (-1)⋅ THEN Reduce 0) THEN Auto THEN MoveToConcl (-1) THEN ListInd (-1)) }

1
1. a : LOSet
2. b : AbDMon
⊢ ∀r2:(|a| × |b|) List. ([] ++ r2 ∈ (|a| × |b|) List)

2
1. a : LOSet
2. b : AbDMon
3. u : |a| × |b|
4. v : (|a| × |b|) List
5. ∀r2:(|a| × |b|) List. (v ++ r2 ∈ (|a| × |b|) List)
⊢ ∀r2:(|a| × |b|) List. ([u / v] ++ r2 ∈ (|a| × |b|) List)

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  rs  :  (|a|  \mtimes{}  |b|)  List  \mtimes{}  ((|a|  \mtimes{}  |b|)  List)
\mvdash{}  (fst(rs))  ++  (snd(rs))  \mmember{}  (|a|  \mtimes{}  |b|)  List


By

---

Latex:
((D  (-1)\mcdot{}  THEN  Reduce  0)  THEN  Auto  THEN  MoveToConcl  (-1)  THEN  ListInd  (-1))

---

Home Index