Proof of Nuprl Lemma : merge-strict-exists

Step * 1 1 1 1 2 of Lemma merge-strict-exists

1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ sorted-by(R;[u / v])
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u u1
14. ∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ [u1 / v1] ⊆ sc ∧ sc ⊆ v @ [u1 / v1])

⊢ ∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ [u1 / v1] ⊆ sc ∧ sc ⊆ [u / v] @ [u1 / v1])

BY
{ (ExRepD THEN With ⌜[u / sc]⌝ (D 0)⋅ THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ sorted-by(R;[u / v])
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u u1
14. sc : T List
15. sorted-by(R;sc)
16. v ⊆ sc
17. [u1 / v1] ⊆ sc
18. sc ⊆ v @ [u1 / v1]
⊢ sorted-by(R;[u / sc])

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ sorted-by(R;[u / v])
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u u1
14. sc : T List
15. sorted-by(R;sc)
16. v ⊆ sc
17. [u1 / v1] ⊆ sc
18. sc ⊆ v @ [u1 / v1]
19. sorted-by(R;[u / sc])
⊢ [u / v] ⊆ [u / sc]

3
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ sorted-by(R;[u / v])
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u u1
14. sc : T List
15. sorted-by(R;sc)
16. v ⊆ sc
17. [u1 / v1] ⊆ sc
18. sc ⊆ v @ [u1 / v1]
19. sorted-by(R;[u / sc])
20. [u / v] ⊆ [u / sc]
⊢ [u1 / v1] ⊆ [u / sc]

4
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;a,b.R a b)
4. u : T
5. v : T List
6. ∀sb:T List
     ((∀a,b:T.  ((a ∈ v) ⇒ (b ∈ sb) ⇒ ((R a b) ∨ (R b a))))
     ⇒ sorted-by(R;v)
     ⇒ sorted-by(R;sb)
     ⇒ (∃sc:T List. (sorted-by(R;sc) ∧ v ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ v @ sb)))
7. u1 : T
8. v1 : T List
9. (∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ v1) ⇒ ((R a b) ∨ (R b a))))
⇒ sorted-by(R;[u / v])
⇒ sorted-by(R;v1)
⇒ (∃sc:T List. (sorted-by(R;sc) ∧ [u / v] ⊆ sc ∧ v1 ⊆ sc ∧ sc ⊆ [u / v] @ v1))
10. ∀a,b:T.  ((a ∈ [u / v]) ⇒ (b ∈ [u1 / v1]) ⇒ ((R a b) ∨ (R b a)))
11. sorted-by(R;[u / v])
12. sorted-by(R;[u1 / v1])
13. R u u1
14. sc : T List
15. sorted-by(R;sc)
16. v ⊆ sc
17. [u1 / v1] ⊆ sc
18. sc ⊆ v @ [u1 / v1]
19. sorted-by(R;[u / sc])
20. [u / v] ⊆ [u / sc]
21. [u1 / v1] ⊆ [u / sc]
⊢ [u / sc] ⊆ [u / v] @ [u1 / v1]

Latex:

Latex:
1. [T] : Type 2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{} 3. Trans(T;a,b.R a b) 4. u : T 5. v : T List 6. \mforall{}sb:T List ((\mforall{}a,b:T. ((a \mmember{} v) {}\mRightarrow{} (b \mmember{} sb) {}\mRightarrow{} ((R a b) \mvee{} (R b a)))) {}\mRightarrow{} sorted-by(R;v) {}\mRightarrow{} sorted-by(R;sb) {}\mRightarrow{} (\mexists{}sc:T List. (sorted-by(R;sc) \mwedge{} v \msubseteq{} sc \mwedge{} sb \msubseteq{} sc \mwedge{} sc \msubseteq{} v @ sb))) 7. u1 : T 8. v1 : T List 9. (\mforall{}a,b:T. ((a \mmember{} [u / v]) {}\mRightarrow{} (b \mmember{} v1) {}\mRightarrow{} ((R a b) \mvee{} (R b a)))) {}\mRightarrow{} sorted-by(R;[u / v]) {}\mRightarrow{} sorted-by(R;v1) {}\mRightarrow{} (\mexists{}sc:T List. (sorted-by(R;sc) \mwedge{} [u / v] \msubseteq{} sc \mwedge{} v1 \msubseteq{} sc \mwedge{} sc \msubseteq{} [u / v] @ v1)) 10. \mforall{}a,b:T. ((a \mmember{} [u / v]) {}\mRightarrow{} (b \mmember{} [u1 / v1]) {}\mRightarrow{} ((R a b) \mvee{} (R b a))) 11. sorted-by(R;[u / v]) 12. sorted-by(R;[u1 / v1]) 13. R u u1 14. \mexists{}sc:T List. (sorted-by(R;sc) \mwedge{} v \msubseteq{} sc \mwedge{} [u1 / v1] \msubseteq{} sc \mwedge{} sc \msubseteq{} v @ [u1 / v1]) \mvdash{} \mexists{}sc:T List. (sorted-by(R;sc) \mwedge{} [u / v] \msubseteq{} sc \mwedge{} [u1 / v1] \msubseteq{} sc \mwedge{} sc \msubseteq{} [u / v] @ [u1 / v1]) By Latex: (ExRepD THEN With \mkleeneopen{}[u / sc]\mkleeneclose{} (D 0)\mcdot{} THEN Auto) Home Index