---

Step * 1 1 1 1 of Lemma oal_merge_sd_ordered


1. a : LOSet
2. b : AbDMon
3. qk : |a|
4. qv : |b|
5. ps' : (|a| × |b|) List
6. pk : |a|
7. pv : |b|
8. qs' : (|a| × |b|) List
9. ∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < ||[<qk, qv> / ps']|| + ||[<pk, pv> / qs']||
     ⇒ (↑sd_ordered(map(λx.(fst(x));us)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));vs)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));us ++ vs))))
10. ↑sd_ordered(map(λx.(fst(x));[<qk, qv> / ps']))
11. ↑sd_ordered(map(λx.(fst(x));[<pk, pv> / qs']))
12. ↑(HTFor{<𝔹,∧b>} v::vs ∈ map(λx.(fst(x));[<pk, pv> / qs']). ∀bw(:|a|) ∈ vs
                                                                  (w <b v))
13. ↑(HTFor{<𝔹,∧b>} v::vs ∈ map(λx.(fst(x));[<qk, qv> / ps']). ∀bw(:|a|) ∈ vs
                                                                  (w <b v))
⊢ ↑(HTFor{<𝔹,∧b>} v::vs ∈ map(λx.(fst(x));[<qk, qv> / ps'] ++ [<pk, pv> / qs']). ∀bw(:|a|) ∈ vs
                                                                                    (w <b v))
BY
{ ((OnMHyps [-1;-2] 
  (\i.AbReduce i THEN RW bool_to_propC i) 
THENM RepD 
THENM OnMHyps [-1;-3] (RWH (RevLemmaC `sd_ordered_char`))) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. qk : |a|
4. qv : |b|
5. ps' : (|a| × |b|) List
6. pk : |a|
7. pv : |b|
8. qs' : (|a| × |b|) List
9. ∀us,vs:(|a| × |b|) List.
     (||us|| + ||vs|| < ||[<qk, qv> / ps']|| + ||[<pk, pv> / qs']||
     ⇒ (↑sd_ordered(map(λx.(fst(x));us)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));vs)))
     ⇒ (↑sd_ordered(map(λx.(fst(x));us ++ vs))))
10. ↑sd_ordered(map(λx.(fst(x));[<qk, qv> / ps']))
11. ↑sd_ordered(map(λx.(fst(x));[<pk, pv> / qs']))
12. ↑(∀bw(:|a|) ∈ map(λx.(fst(x));qs')
         (w <b pk))
13. ↑sd_ordered(map(λx.(fst(x));qs'))
14. ↑(∀bw(:|a|) ∈ map(λx.(fst(x));ps')
         (w <b qk))
15. ↑sd_ordered(map(λx.(fst(x));ps'))
⊢ ↑(HTFor{<𝔹,∧b>} v::vs ∈ map(λx.(fst(x));[<qk, qv> / ps'] ++ [<pk, pv> / qs']). ∀bw(:|a|) ∈ vs
                                                                                    (w <b v))

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDMon
3.  qk  :  |a|
4.  qv  :  |b|
5.  ps'  :  (|a|  \mtimes{}  |b|)  List
6.  pk  :  |a|
7.  pv  :  |b|
8.  qs'  :  (|a|  \mtimes{}  |b|)  List
9.  \mforall{}us,vs:(|a|  \mtimes{}  |b|)  List.
          (||us||  +  ||vs||  <  ||[<qk,  qv>  /  ps']||  +  ||[<pk,  pv>  /  qs']||
          {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));us)))
          {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));vs)))
          {}\mRightarrow{}  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));us  ++  vs))))
10.  \muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));[<qk,  qv>  /  ps']))
11.  \muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));[<pk,  pv>  /  qs']))
12.  \muparrow{}(HTFor\{<\mBbbB{},\mwedge{}\msubb{}>\}  v::vs  \mmember{}  map(\mlambda{}x.(fst(x));[<pk,  pv>  /  qs']).  \mforall{}\msubb{}w(:|a|)  \mmember{}  vs
                                                                                                                                    (w  <\msubb{}  v))
13.  \muparrow{}(HTFor\{<\mBbbB{},\mwedge{}\msubb{}>\}  v::vs  \mmember{}  map(\mlambda{}x.(fst(x));[<qk,  qv>  /  ps']).  \mforall{}\msubb{}w(:|a|)  \mmember{}  vs
                                                                                                                                    (w  <\msubb{}  v))
\mvdash{}  \muparrow{}(HTFor\{<\mBbbB{},\mwedge{}\msubb{}>\}  v::vs  \mmember{}  map(\mlambda{}x.(fst(x));[<qk,  qv>  /  ps']  ++  [<pk,  pv>  /  qs']).  \mforall{}\msubb{}w(:|a|)  \mmember{}  vs
                                                                                                                                                                        (w  <\msubb{}  v))


By

---

Latex:
((OnMHyps  [-1;-2] 
    (\mbackslash{}i.AbReduce  i  THEN  RW  bool\_to\_propC  i) 
THENM  RepD 
THENM  OnMHyps  [-1;-3]  (RWH  (RevLemmaC  `sd\_ordered\_char`)))  THENA  Auto)

---

Home Index