Step
*
1
1
1
2
of Lemma
Q-R-glues-split
1. [Info] : Type
2. [P] : es:EO+(Info) ─→ E ─→ ℙ
3. p : ∀es:EO+(Info). ∀e:E. Dec(P[es;e])@i'
4. [A] : Type
5. [B] : Type
6. Ia : EClass(A)@i'
7. Ib : EClass(B)@i'
8. Singlevalued(Ia) ∧ Singlevalued(Ib)@i'
9. g1 : es:EO+(Info) ─→ E(Ib) ─→ E@i'
10. q : ∀es:EO+(Info). ∀e:E. Dec((↑e ∈b Ib) c∧ P[es;g1 es e])@i'
11. es : EO+(Info)@i'
12. [Q] : E ─→ E ─→ ℙ
13. [R] : E ─→ E ─→ ℙ
14. ∀x,y:E. ((Q x y) ⇒ (P[es;x] ⇐⇒ P[es;y]))@i
15. f : E(Ia) ─→ B@i
16. g2 : E(Ib) ─→ E@i
17. g1 es glues (Ia|p):Q ──f─→ (Ib|q):R@i
18. g2 glues (Ia|¬p):Q ──f─→ (Ib|¬q):R@i
19. (E((Ib|q)) ⊆r E(Ib)) ∧ (E((Ia|p)) ⊆r E(Ia))
20. (E((Ia|¬p)) ⊆r E(Ia)) ∧ (E((Ib|¬q)) ⊆r E(Ib))
21. [{(Ib|q)}? g1 es : g2] glues [(Ia|p)?(Ia|¬p)]:Q|{(Ia|p)} ∨ Q|{(Ia|¬p)} ──f─→ [(Ib|q)?(Ib|¬q)]:R
22. Q ⇐⇒ Q|{(Ia|p)} ∨ Q|{(Ia|¬p)}
⊢ [λe.P[es;g1 es e]? g1 es : g2] glues Ia:Q ──f─→ Ib:R
BY
{ Assert ⌈[λe.P[es;g1 es e]? g1 es : g2] = [{(Ib|q)}? g1 es : g2] ∈ (E(Ib) ─→ E)⌉⋅ }
1
.....assertion.....
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ ℙ
3. p : ∀es:EO+(Info). ∀e:E. Dec(P[es;e])@i'
4. A : Type
5. B : Type
6. Ia : EClass(A)@i'
7. Ib : EClass(B)@i'
8. Singlevalued(Ia) ∧ Singlevalued(Ib)@i'
9. g1 : es:EO+(Info) ─→ E(Ib) ─→ E@i'
10. q : ∀es:EO+(Info). ∀e:E. Dec((↑e ∈b Ib) c∧ P[es;g1 es e])@i'
11. es : EO+(Info)@i'
12. Q : E ─→ E ─→ ℙ
13. R : E ─→ E ─→ ℙ
14. ∀x,y:E. ((Q x y) ⇒ (P[es;x] ⇐⇒ P[es;y]))@i
15. f : E(Ia) ─→ B@i
16. g2 : E(Ib) ─→ E@i
17. g1 es glues (Ia|p):Q ──f─→ (Ib|q):R@i
18. g2 glues (Ia|¬p):Q ──f─→ (Ib|¬q):R@i
19. (E((Ib|q)) ⊆r E(Ib)) ∧ (E((Ia|p)) ⊆r E(Ia))
20. (E((Ia|¬p)) ⊆r E(Ia)) ∧ (E((Ib|¬q)) ⊆r E(Ib))
21. [{(Ib|q)}? g1 es : g2] glues [(Ia|p)?(Ia|¬p)]:Q|{(Ia|p)} ∨ Q|{(Ia|¬p)} ──f─→ [(Ib|q)?(Ib|¬q)]:R
22. Q ⇐⇒ Q|{(Ia|p)} ∨ Q|{(Ia|¬p)}
⊢ [λe.P[es;g1 es e]? g1 es : g2] = [{(Ib|q)}? g1 es : g2] ∈ (E(Ib) ─→ E)
2
1. [Info] : Type
2. [P] : es:EO+(Info) ─→ E ─→ ℙ
3. p : ∀es:EO+(Info). ∀e:E. Dec(P[es;e])@i'
4. [A] : Type
5. [B] : Type
6. Ia : EClass(A)@i'
7. Ib : EClass(B)@i'
8. Singlevalued(Ia) ∧ Singlevalued(Ib)@i'
9. g1 : es:EO+(Info) ─→ E(Ib) ─→ E@i'
10. q : ∀es:EO+(Info). ∀e:E. Dec((↑e ∈b Ib) c∧ P[es;g1 es e])@i'
11. es : EO+(Info)@i'
12. [Q] : E ─→ E ─→ ℙ
13. [R] : E ─→ E ─→ ℙ
14. ∀x,y:E. ((Q x y) ⇒ (P[es;x] ⇐⇒ P[es;y]))@i
15. f : E(Ia) ─→ B@i
16. g2 : E(Ib) ─→ E@i
17. g1 es glues (Ia|p):Q ──f─→ (Ib|q):R@i
18. g2 glues (Ia|¬p):Q ──f─→ (Ib|¬q):R@i
19. (E((Ib|q)) ⊆r E(Ib)) ∧ (E((Ia|p)) ⊆r E(Ia))
20. (E((Ia|¬p)) ⊆r E(Ia)) ∧ (E((Ib|¬q)) ⊆r E(Ib))
21. [{(Ib|q)}? g1 es : g2] glues [(Ia|p)?(Ia|¬p)]:Q|{(Ia|p)} ∨ Q|{(Ia|¬p)} ──f─→ [(Ib|q)?(Ib|¬q)]:R
22. Q ⇐⇒ Q|{(Ia|p)} ∨ Q|{(Ia|¬p)}
23. [λe.P[es;g1 es e]? g1 es : g2] = [{(Ib|q)}? g1 es : g2] ∈ (E(Ib) ─→ E)
⊢ [λe.P[es;g1 es e]? g1 es : g2] glues Ia:Q ──f─→ Ib:R
Latex:
Latex:
1. [Info] : Type
2. [P] : es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
3. p : \mforall{}es:EO+(Info). \mforall{}e:E. Dec(P[es;e])@i'
4. [A] : Type
5. [B] : Type
6. Ia : EClass(A)@i'
7. Ib : EClass(B)@i'
8. Singlevalued(Ia) \mwedge{} Singlevalued(Ib)@i'
9. g1 : es:EO+(Info) {}\mrightarrow{} E(Ib) {}\mrightarrow{} E@i'
10. q : \mforall{}es:EO+(Info). \mforall{}e:E. Dec((\muparrow{}e \mmember{}\msubb{} Ib) c\mwedge{} P[es;g1 es e])@i'
11. es : EO+(Info)@i'
12. [Q] : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
13. [R] : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
14. \mforall{}x,y:E. ((Q x y) {}\mRightarrow{} (P[es;x] \mLeftarrow{}{}\mRightarrow{} P[es;y]))@i
15. f : E(Ia) {}\mrightarrow{} B@i
16. g2 : E(Ib) {}\mrightarrow{} E@i
17. g1 es glues (Ia|p):Q {}{}f{}\mrightarrow{} (Ib|q):R@i
18. g2 glues (Ia|\mneg{}p):Q {}{}f{}\mrightarrow{} (Ib|\mneg{}q):R@i
19. (E((Ib|q)) \msubseteq{}r E(Ib)) \mwedge{} (E((Ia|p)) \msubseteq{}r E(Ia))
20. (E((Ia|\mneg{}p)) \msubseteq{}r E(Ia)) \mwedge{} (E((Ib|\mneg{}q)) \msubseteq{}r E(Ib))
21. [\{(Ib|q)\}? g1 es : g2] glues [(Ia|p)?(Ia|\mneg{}p)]:Q|\{(Ia|p)\} \mvee{} Q|\{(Ia|\mneg{}p)\} {}{}f{}\mrightarrow{} [(Ib|q)?(Ib|\mneg{}q)]:R
22. Q \mLeftarrow{}{}\mRightarrow{} Q|\{(Ia|p)\} \mvee{} Q|\{(Ia|\mneg{}p)\}
\mvdash{} [\mlambda{}e.P[es;g1 es e]? g1 es : g2] glues Ia:Q {}{}f{}\mrightarrow{} Ib:R
By
Latex:
Assert \mkleeneopen{}[\mlambda{}e.P[es;g1 es e]? g1 es : g2] = [\{(Ib|q)\}? g1 es : g2]\mkleeneclose{}\mcdot{}
Home
Index