---

Step * of Lemma oal_merge_dom_pred

∀a:LOSet. ∀b:AbDMon. ∀Q:|a| ⟶ 𝔹. ∀ps,qs:(|a| × |b|) List.
  ((↑(∀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
{ ((RepeatMFor 3 (D 0) 
THENM BLemma `list_pr_length_ind` 
THENM D 0 THENM D 0) THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}Q:|a|  {}\mrightarrow{}  \mBbbB{}.  \mforall{}ps,qs:(|a|  \mtimes{}  |b|)  List.
    ((\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:
((RepeatMFor  3  (D  0) 
THENM  BLemma  `list\_pr\_length\_ind` 
THENM  D  0  THENM  D  0)  THENA  Auto)

---

Home Index