Step * 1 of Lemma oal_merge_dom_pred


1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. ps (|a| × |b|) List
5. qs (|a| × |b|) List
⊢ (∀us,vs:(|a| × |b|) List.
     (||us|| ||vs|| < ||ps|| ||qs||
      (↑(∀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]))))
 (↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps)
         Q[x]))
 (↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs)
         Q[x]))
 (↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps ++ qs)
         Q[x]))
BY
New [`q';`qs\''] (D 5) 
THEN New [`p';`ps\''] (D 4) 
THEN ((AbReduce 0) THEN Auto)⋅ }

1
1. LOSet
2. AbDMon
3. |a| ⟶ 𝔹
4. |a| × |b|
5. ps' (|a| × |b|) List
6. |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])


Latex:


Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  Q  :  |a|  {}\mrightarrow{}  \mBbbB{}
4.  ps  :  (|a|  \mtimes{}  |b|)  List
5.  qs  :  (|a|  \mtimes{}  |b|)  List
\mvdash{}  (\mforall{}us,vs:(|a|  \mtimes{}  |b|)  List.
          (||us||  +  ||vs||  <  ||ps||  +  ||qs||
          {}\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]))))
{}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));ps)
                  Q[x]))
{}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));qs)
                  Q[x]))
{}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}x.(fst(x));ps  ++  qs)
                  Q[x]))


By


Latex:
New  [`q';`qs\mbackslash{}'']  (D  5) 
THEN  New  [`p';`ps\mbackslash{}'']  (D  4) 
THEN  ((AbReduce  0)  THEN  Auto)\mcdot{}




Home Index