---

Step * 1 1 1 3 of Lemma oal_merge_non_id_vals

.....truecase..... 
1. a : LOSet
2. b : AbDMon
3. qk : |a|
4. qv : |b|
5. ps' : (|a| × |b|) List
6. pk : |a|
7. pv : |b|
8. qs' : (|a| × |b|) List
9. ∀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))))
10. ¬(qv = e ∈ |b|)
11. ¬↑(e ∈b map(λx.(snd(x));ps'))
12. ¬(pv = e ∈ |b|)
13. ¬↑(e ∈b map(λx.(snd(x));qs'))
14. ¬(pk <a qk)
15. ¬(qk <a pk)
16. (qv * pv) = e ∈ |b|
⊢ ¬↑(e ∈b map(λx.(snd(x));ps' ++ qs'))
BY
{ Repeat (First 
 [Progress (AbReduce 0) 
 ;Progress ((RW (RevLemmaC `assert_of_bnot` 
    ANDTHENC (SubC (LemmaC `bnot_thru_bor`))) 0) THENA Auto) 
 ;Progress ((RW bool_to_propC 0) THENA Auto) 
 ;Progress Auto 
 ;BHyp 9]) }

---

Latex:

---

Latex:
.....truecase..... 
1.  a  :  LOSet
2.  b  :  AbDMon
3.  qk  :  |a|
4.  qv  :  |b|
5.  ps'  :  (|a|  \mtimes{}  |b|)  List
6.  pk  :  |a|
7.  pv  :  |b|
8.  qs'  :  (|a|  \mtimes{}  |b|)  List
9.  \mforall{}us,vs:(|a|  \mtimes{}  |b|)  List.
          (||us||  +  ||vs||  <  (||ps'||  +  1)  +  ||qs'||  +  1
          {}\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))))
10.  \mneg{}(qv  =  e)
11.  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps'))
12.  \mneg{}(pv  =  e)
13.  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs'))
14.  \mneg{}(pk  <a  qk)
15.  \mneg{}(qk  <a  pk)
16.  (qv  *  pv)  =  e
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps'  ++  qs'))


By

---

Latex:
Repeat  (First 
  [Progress  (AbReduce  0) 
  ;Progress  ((RW  (RevLemmaC  `assert\_of\_bnot` 
        ANDTHENC  (SubC  (LemmaC  `bnot\_thru\_bor`)))  0)  THENA  Auto) 
  ;Progress  ((RW  bool\_to\_propC  0)  THENA  Auto) 
  ;Progress  Auto 
  ;BHyp  9])

---

Home Index