Step
*
1
1
1
2
1
1
of Lemma
Q-R-glues-split
.....subterm..... T:t
1:n
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. x : E(Ib)@i
⊢ if p:P[es;g1 es x] then g1 es x else g2 x fi = if p:{(Ib|q)} x then g1 es x else g2 x fi ∈ E
BY
{ (RepUR ``es-interface-predicate`` 0 THEN RepeatFor 2 ((Branch 0 THENA Try (Complete (Auto)))) THEN Auto) }
1
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)@i'
9. Singlevalued(Ib)@i'
10. g1 : es:EO+(Info) ─→ E(Ib) ─→ E@i'
11. q : ∀es:EO+(Info). ∀e:E. Dec((↑e ∈b Ib) c∧ P[es;g1 es e])@i'
12. es : EO+(Info)@i'
13. Q : E ─→ E ─→ ℙ
14. R : E ─→ E ─→ ℙ
15. ∀x,y:E. ((Q x y) ⇒ (P[es;x] ⇐⇒ P[es;y]))@i
16. f : E(Ia) ─→ B@i
17. g2 : E(Ib) ─→ E@i
18. g1 es glues (Ia|p):Q ──f─→ (Ib|q):R@i
19. g2 glues (Ia|¬p):Q ──f─→ (Ib|¬q):R@i
20. E((Ib|q)) ⊆r E(Ib)
21. E((Ia|p)) ⊆r E(Ia)
22. E((Ia|¬p)) ⊆r E(Ia)
23. E((Ib|¬q)) ⊆r E(Ib)
24. [{(Ib|q)}? g1 es : g2] glues [(Ia|p)?(Ia|¬p)]:Q|{(Ia|p)} ∨ Q|{(Ia|¬p)} ──f─→ [(Ib|q)?(Ib|¬q)]:R
25. Q ⇐⇒ Q|{(Ia|p)} ∨ Q|{(Ia|¬p)}
26. x : E(Ib)@i
27. x1 : P[es;g1 es x]@i
28. (p es (g1 es x)) = (inl x1) ∈ Dec(P[es;g1 es x])@i
29. y : ¬↑x ∈b (Ib|q)@i
30. bool-decider(x ∈b (Ib|q)) = (inr y ) ∈ Dec(↑x ∈b (Ib|q))@i
⊢ (g1 es x) = (g2 x) ∈ 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)@i'
9. Singlevalued(Ib)@i'
10. g1 : es:EO+(Info) ─→ E(Ib) ─→ E@i'
11. q : ∀es:EO+(Info). ∀e:E. Dec((↑e ∈b Ib) c∧ P[es;g1 es e])@i'
12. es : EO+(Info)@i'
13. Q : E ─→ E ─→ ℙ
14. R : E ─→ E ─→ ℙ
15. ∀x,y:E. ((Q x y) ⇒ (P[es;x] ⇐⇒ P[es;y]))@i
16. f : E(Ia) ─→ B@i
17. g2 : E(Ib) ─→ E@i
18. g1 es glues (Ia|p):Q ──f─→ (Ib|q):R@i
19. g2 glues (Ia|¬p):Q ──f─→ (Ib|¬q):R@i
20. E((Ib|q)) ⊆r E(Ib)
21. E((Ia|p)) ⊆r E(Ia)
22. E((Ia|¬p)) ⊆r E(Ia)
23. E((Ib|¬q)) ⊆r E(Ib)
24. [{(Ib|q)}? g1 es : g2] glues [(Ia|p)?(Ia|¬p)]:Q|{(Ia|p)} ∨ Q|{(Ia|¬p)} ──f─→ [(Ib|q)?(Ib|¬q)]:R
25. Q ⇐⇒ Q|{(Ia|p)} ∨ Q|{(Ia|¬p)}
26. x : E(Ib)@i
27. y : ¬P[es;g1 es x]@i
28. (p es (g1 es x)) = (inr y ) ∈ Dec(P[es;g1 es x])@i
29. x1 : ↑x ∈b (Ib|q)@i
30. bool-decider(x ∈b (Ib|q)) = (inl x1) ∈ Dec(↑x ∈b (Ib|q))@i
⊢ (g2 x) = (g1 es x) ∈ E
Latex:
Latex:
.....subterm..... T:t
1:n
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)\}
23. x : E(Ib)@i
\mvdash{} if p:P[es;g1 es x] then g1 es x else g2 x fi = if p:\{(Ib|q)\} x then g1 es x else g2 x fi
By
Latex:
(RepUR ``es-interface-predicate`` 0
THEN RepeatFor 2 ((Branch 0 THENA Try (Complete (Auto))))
THEN Auto)
Home
Index