---

Step * 1 1 of Lemma oal_merge_dom_pred


1. a : LOSet
2. b : AbDMon
3. Q : |a| ⟶ 𝔹
4. p : |a| × |b|
5. ps' : (|a| × |b|) List
6. q : |a| × |b|
7. qs' : (|a| × |b|) List
8. ∀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])))
9. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps')
        Q[x])
10. ↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs')
         Q[x])
11. ↑Q[fst(q)]
12. ↑Q[fst(p)]
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[p / ps'] ++ [q / qs'])
       Q[x])
BY
{ New [`pk';`pv'] (D 6) 
THEN New [`qk';`qv'] (D 4) 
THEN (( OnMHyps [-1;-2]  
  (\i.AbReduce i THEN RW bool_to_propC i)) THENA Auto) 
THEN RepD }

1
1. a : LOSet
2. b : AbDMon
3. Q : |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])

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  Q  :  |a|  {}\mrightarrow{}  \mBbbB{}
4.  p  :  |a|  \mtimes{}  |b|
5.  ps'  :  (|a|  \mtimes{}  |b|)  List
6.  q  :  |a|  \mtimes{}  |b|
7.  qs'  :  (|a|  \mtimes{}  |b|)  List
8.  \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])))
9.  \muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));ps')
                Q[x])
10.  \muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));qs')
                  Q[x])
11.  \muparrow{}Q[fst(q)]
12.  \muparrow{}Q[fst(p)]
\mvdash{}  \muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));[p  /  ps']  ++  [q  /  qs'])
              Q[x])


By

---

Latex:
New  [`pk';`pv']  (D  6) 
THEN  New  [`qk';`qv']  (D  4) 
THEN  ((  OnMHyps  [-1;-2]   
    (\mbackslash{}i.AbReduce  i  THEN  RW  bool\_to\_propC  i))  THENA  Auto) 
THEN  RepD

---

Home Index