---

Step * 1 1 1 of Lemma oal_merge_non_id_vals


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']))
BY
{ AbReduce 0 
THEN ((RepeatM SplitOnConclITE) THENA Auto) }

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

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

3
.....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'))

4
.....falsecase..... 
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));[<qk, qv * pv> / (ps' ++ qs')]))

---

Latex:

---

Latex:

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'))
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));[<qk,  qv>  /  ps']  ++  [<pk,  pv>  /  qs']))


By

---

Latex:
AbReduce  0 
THEN  ((RepeatM  SplitOnConclITE)  THENA  Auto)

---

Home Index