Step
*
1
1
1
of Lemma
oal_merge_dom_pred
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])
BY
{ AbReduce 0
THEN ((RepeatM SplitOnConclITE) THENA Auto) }
1
.....truecase.....
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]
15. pk <a qk
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[<qk, qv> / (ps' ++ [<pk, pv> / qs'])])
Q[x])
2
.....truecase.....
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]
15. ¬(pk <a qk)
16. qk <a pk
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));[<pk, pv> / ([<qk, qv> / ps'] ++ qs')])
Q[x])
3
.....truecase.....
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]
15. ¬(pk <a qk)
16. ¬(qk <a pk)
17. (qv * pv) = e ∈ |b|
⊢ ↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps' ++ qs')
Q[x])
4
.....falsecase.....
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]
15. ¬(pk <a qk)
16. ¬(qk <a 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