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