---

Step * 1 of Lemma oal_merge_non_id_vals


1. a : LOSet
2. b : AbDMon
3. ps : (|a| × |b|) List
4. qs : (|a| × |b|) List
⊢ (∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < ||ps|| + ||qs||
     ⇒ (¬↑(e ∈b map(λx.(snd(x));us)))
     ⇒ (¬↑(e ∈b map(λx.(snd(x));vs)))
     ⇒ (¬↑(e ∈b map(λx.(snd(x));us ++ vs)))))
⇒ (¬↑(e ∈b map(λx.(snd(x));ps)))
⇒ (¬↑(e ∈b map(λx.(snd(x));qs)))
⇒ (¬↑(e ∈b map(λx.(snd(x));ps ++ qs)))
BY
{ New [`q';`qs\''] (D 4) 
THEN New [`p';`ps\''] (D 3) 
THEN ((AbReduce 0) THEN Auto)⋅ }

1
1. a : LOSet
2. b : AbDMon
3. p : |a| × |b|
4. ps' : (|a| × |b|) List
5. q : |a| × |b|
6. qs' : (|a| × |b|) List
7. ∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < (||ps'|| + 1) + ||qs'|| + 1
     ⇒ (¬↑(e ∈b map(λx.(snd(x));us)))
     ⇒ (¬↑(e ∈b map(λx.(snd(x));vs)))
     ⇒ (¬↑(e ∈b map(λx.(snd(x));us ++ vs))))
8. ¬↑(((snd(p)) =b e) ∨b(e ∈b map(λx.(snd(x));ps')))
9. ¬↑(((snd(q)) =b e) ∨b(e ∈b map(λx.(snd(x));qs')))
⊢ ¬↑(e ∈b map(λx.(snd(x));[p / ps'] ++ [q / qs']))

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  ps  :  (|a|  \mtimes{}  |b|)  List
4.  qs  :  (|a|  \mtimes{}  |b|)  List
\mvdash{}  (\mforall{}us,vs:(|a|  \mtimes{}  |b|)  List.
          (||us||  +  ||vs||  <  ||ps||  +  ||qs||
          {}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));us)))
          {}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));vs)))
          {}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));us  ++  vs)))))
{}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
{}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs)))
{}\mRightarrow{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps  ++  qs)))


By

---

Latex:
New  [`q';`qs\mbackslash{}'']  (D  4) 
THEN  New  [`p';`ps\mbackslash{}'']  (D  3) 
THEN  ((AbReduce  0)  THEN  Auto)\mcdot{}

---

Home Index