---

Step * 1 1 of Lemma oal_merge_non_id_vals


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']))
BY
{ New [`pk';`pv'] (D 5) 
THEN New [`qk';`qv'] (D 3) 
% fiddly stuff! % 
THEN ( OnMHyps [-1;-2]  
  (\i. 
    AbReduce i  
    THENM RWH (RevLemmaC `assert_of_bnot`) i 
    THENM RWH (LemmaC `bnot_thru_bor`) i 
    THENM RW bool_to_propC i 
  ) THENA Auto) 
THEN RepD⋅ }

1
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'))
⊢ ¬↑(e ∈b map(λx.(snd(x));[<qk, qv> / ps'] ++ [<pk, pv> / qs']))

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  p  :  |a|  \mtimes{}  |b|
4.  ps'  :  (|a|  \mtimes{}  |b|)  List
5.  q  :  |a|  \mtimes{}  |b|
6.  qs'  :  (|a|  \mtimes{}  |b|)  List
7.  \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))))
8.  \mneg{}\muparrow{}(((snd(p))  =\msubb{}  e)  \mvee{}\msubb{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps')))
9.  \mneg{}\muparrow{}(((snd(q))  =\msubb{}  e)  \mvee{}\msubb{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs')))
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));[p  /  ps']  ++  [q  /  qs']))


By

---

Latex:
New  [`pk';`pv']  (D  5) 
THEN  New  [`qk';`qv']  (D  3) 
\%  fiddly  stuff!  \% 
THEN  (  OnMHyps  [-1;-2]   
    (\mbackslash{}i. 
        AbReduce  i   
        THENM  RWH  (RevLemmaC  `assert\_of\_bnot`)  i 
        THENM  RWH  (LemmaC  `bnot\_thru\_bor`)  i 
        THENM  RW  bool\_to\_propC  i 
    )  THENA  Auto) 
THEN  RepD\mcdot{}

---

Home Index