Step * 1 1 1 of Lemma oal_merge_dom_pred


1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. qk |a|
5. qv |b|
6. ps' (|a| × |b|) List
7. pk |a|
8. pv |b|
9. qs' (|a| × |b|) List
10. ∀us,vs:(|a| × |b|) List.
      (||us|| ||vs|| < (||ps'|| 1) ||qs'|| 1
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));vs)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us ++ vs)
               Q[x])))
11. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps')
         Q[x])
12. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs')
         Q[x])
13. ↑Q[pk]
14. ↑Q[qk]
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[<qk, qv> ps'] ++ [<pk, pv> qs'])
       Q[x])
BY
AbReduce 
THEN ((RepeatM SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. qk |a|
5. qv |b|
6. ps' (|a| × |b|) List
7. pk |a|
8. pv |b|
9. qs' (|a| × |b|) List
10. ∀us,vs:(|a| × |b|) List.
      (||us|| ||vs|| < (||ps'|| 1) ||qs'|| 1
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));vs)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us ++ vs)
               Q[x])))
11. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps')
         Q[x])
12. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs')
         Q[x])
13. ↑Q[pk]
14. ↑Q[qk]
15. pk <qk
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[<qk, qv> (ps' ++ [<pk, pv> qs'])])
       Q[x])

2
.....truecase..... 
1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. qk |a|
5. qv |b|
6. ps' (|a| × |b|) List
7. pk |a|
8. pv |b|
9. qs' (|a| × |b|) List
10. ∀us,vs:(|a| × |b|) List.
      (||us|| ||vs|| < (||ps'|| 1) ||qs'|| 1
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));vs)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us ++ vs)
               Q[x])))
11. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps')
         Q[x])
12. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs')
         Q[x])
13. ↑Q[pk]
14. ↑Q[qk]
15. ¬(pk <qk)
16. qk <pk
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[<pk, pv> ([<qk, qv> ps'] ++ qs')])
       Q[x])

3
.....truecase..... 
1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. qk |a|
5. qv |b|
6. ps' (|a| × |b|) List
7. pk |a|
8. pv |b|
9. qs' (|a| × |b|) List
10. ∀us,vs:(|a| × |b|) List.
      (||us|| ||vs|| < (||ps'|| 1) ||qs'|| 1
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));vs)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us ++ vs)
               Q[x])))
11. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps')
         Q[x])
12. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs')
         Q[x])
13. ↑Q[pk]
14. ↑Q[qk]
15. ¬(pk <qk)
16. ¬(qk <pk)
17. (qv pv) e ∈ |b|
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps' ++ qs')
       Q[x])

4
.....falsecase..... 
1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. qk |a|
5. qv |b|
6. ps' (|a| × |b|) List
7. pk |a|
8. pv |b|
9. qs' (|a| × |b|) List
10. ∀us,vs:(|a| × |b|) List.
      (||us|| ||vs|| < (||ps'|| 1) ||qs'|| 1
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));vs)
               Q[x]))
       (↑(∀bx(:|a|) ∈ map(λx.(fst(x));us ++ vs)
               Q[x])))
11. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps')
         Q[x])
12. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs')
         Q[x])
13. ↑Q[pk]
14. ↑Q[qk]
15. ¬(pk <qk)
16. ¬(qk <pk)
17. ¬((qv pv) e ∈ |b|)
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[<qk, qv pv> (ps' ++ qs')])
       Q[x])


Latex:


Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  Q  :  |a|  {}\mrightarrow{}  \mBbbB{}
4.  qk  :  |a|
5.  qv  :  |b|
6.  ps'  :  (|a|  \mtimes{}  |b|)  List
7.  pk  :  |a|
8.  pv  :  |b|
9.  qs'  :  (|a|  \mtimes{}  |b|)  List
10.  \mforall{}us,vs:(|a|  \mtimes{}  |b|)  List.
            (||us||  +  ||vs||  <  (||ps'||  +  1)  +  ||qs'||  +  1
            {}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));us)
                              Q[x]))
            {}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));vs)
                              Q[x]))
            {}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));us  ++  vs)
                              Q[x])))
11.  \muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));ps')
                  Q[x])
12.  \muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));qs')
                  Q[x])
13.  \muparrow{}Q[pk]
14.  \muparrow{}Q[qk]
\mvdash{}  \muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));[<qk,  qv>  /  ps']  ++  [<pk,  pv>  /  qs'])
              Q[x])


By


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




Home Index