Step
*
1
3
1
1
of Lemma
Q-R-glues-conditional
1. Info : Type
2. es : EO+(Info)@i'
3. Q1 : E ─→ E ─→ ℙ
4. Q2 : E ─→ E ─→ ℙ
5. R : E ─→ E ─→ ℙ
6. A : Type
7. B : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) ─→ B@i
13. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. λe.(↑e ∈b Ia1) ←←= g1== λe.(↑e ∈b Ib1)@i
18. g1 is Q1-R-pre-preserving on λe.(↑e ∈b Ib1)@i
19. ∀a1,a2:E(Ib1). (((g1 a1) = (g1 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib1)))@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. λe.(↑e ∈b Ia2) ←←= g2== λe.(↑e ∈b Ib2)@i
22. g2 is Q2-R-pre-preserving on λe.(↑e ∈b Ib2)@i
23. ∀a1,a2:E(Ib2). (((g2 a1) = (g2 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib2)))@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. λe.(↑e ∈b [Ia1?Ia2]) ←←= [λe.(↑e ∈b Ib1)? g1 : g2]== λe.(↑e ∈b [Ib1?Ib2])
26. [λe.(↑e ∈b Ib1)? g1 : g2] is Q1|λe.(↑e ∈b Ia1) ∨ Q2|λe.(↑e ∈b Ia2)-R-pre-preserving on λe.(↑e ∈b [Ib1?Ib2])
27. a1 : E([Ib1?Ib2])@i
28. a2 : E([Ib1?Ib2])@i
29. ([λe.(↑e ∈b Ib1)? g1 : g2] a1) = ([λe.(↑e ∈b Ib1)? g1 : g2] a2) ∈ E@i
⊢ a1 = a2 ∈ E([Ib1?Ib2])
BY
{ (RepUR ``conditional`` (-1) THEN Branch (-1)) }
1
.....wf.....
1. Info : Type
2. es : EO+(Info)@i'
3. Q1 : E ─→ E ─→ ℙ
4. Q2 : E ─→ E ─→ ℙ
5. R : E ─→ E ─→ ℙ
6. A : Type
7. B : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) ─→ B@i
13. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. λe.(↑e ∈b Ia1) ←←= g1== λe.(↑e ∈b Ib1)@i
18. g1 is Q1-R-pre-preserving on λe.(↑e ∈b Ib1)@i
19. ∀a1,a2:E(Ib1). (((g1 a1) = (g1 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib1)))@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. λe.(↑e ∈b Ia2) ←←= g2== λe.(↑e ∈b Ib2)@i
22. g2 is Q2-R-pre-preserving on λe.(↑e ∈b Ib2)@i
23. ∀a1,a2:E(Ib2). (((g2 a1) = (g2 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib2)))@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. λe.(↑e ∈b [Ia1?Ia2]) ←←= [λe.(↑e ∈b Ib1)? g1 : g2]== λe.(↑e ∈b [Ib1?Ib2])
26. [λe.(↑e ∈b Ib1)? g1 : g2] is Q1|λe.(↑e ∈b Ia1) ∨ Q2|λe.(↑e ∈b Ia2)-R-pre-preserving on λe.(↑e ∈b [Ib1?Ib2])
27. a1 : E([Ib1?Ib2])@i
28. a2 : E([Ib1?Ib2])@i
29. z : Dec(↑a1 ∈b Ib1)
30. bool-decider(a1 ∈b Ib1) = z ∈ Dec(↑a1 ∈b Ib1)
31. case bool-decider(a1 ∈b Ib1) of inl(p) => g1 a1 | inr(x) => g2 a1 = if p:↑a2 ∈b Ib1 then g1 a2 else g2 a2 fi ∈ E@i
32. z1 : Dec(↑a1 ∈b Ib1)
⊢ case z1 of inl(p) => g1 a1 | inr(x) => g2 a1 = if p:↑a2 ∈b Ib1 then g1 a2 else g2 a2 fi ∈ E ∈ ℙ
2
1. Info : Type
2. es : EO+(Info)@i'
3. Q1 : E ─→ E ─→ ℙ
4. Q2 : E ─→ E ─→ ℙ
5. R : E ─→ E ─→ ℙ
6. A : Type
7. B : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) ─→ B@i
13. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. λe.(↑e ∈b Ia1) ←←= g1== λe.(↑e ∈b Ib1)@i
18. g1 is Q1-R-pre-preserving on λe.(↑e ∈b Ib1)@i
19. ∀a1,a2:E(Ib1). (((g1 a1) = (g1 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib1)))@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. λe.(↑e ∈b Ia2) ←←= g2== λe.(↑e ∈b Ib2)@i
22. g2 is Q2-R-pre-preserving on λe.(↑e ∈b Ib2)@i
23. ∀a1,a2:E(Ib2). (((g2 a1) = (g2 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib2)))@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. λe.(↑e ∈b [Ia1?Ia2]) ←←= [λe.(↑e ∈b Ib1)? g1 : g2]== λe.(↑e ∈b [Ib1?Ib2])
26. [λe.(↑e ∈b Ib1)? g1 : g2] is Q1|λe.(↑e ∈b Ia1) ∨ Q2|λe.(↑e ∈b Ia2)-R-pre-preserving on λe.(↑e ∈b [Ib1?Ib2])
27. a1 : E([Ib1?Ib2])@i
28. a2 : E([Ib1?Ib2])@i
29. x : ↑a1 ∈b Ib1
30. bool-decider(a1 ∈b Ib1) = (inl x) ∈ Dec(↑a1 ∈b Ib1)
31. (g1 a1) = if p:↑a2 ∈b Ib1 then g1 a2 else g2 a2 fi ∈ E
⊢ a1 = a2 ∈ E([Ib1?Ib2])
3
1. Info : Type
2. es : EO+(Info)@i'
3. Q1 : E ─→ E ─→ ℙ
4. Q2 : E ─→ E ─→ ℙ
5. R : E ─→ E ─→ ℙ
6. A : Type
7. B : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) ─→ B@i
13. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. λe.(↑e ∈b Ia1) ←←= g1== λe.(↑e ∈b Ib1)@i
18. g1 is Q1-R-pre-preserving on λe.(↑e ∈b Ib1)@i
19. ∀a1,a2:E(Ib1). (((g1 a1) = (g1 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib1)))@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. λe.(↑e ∈b Ia2) ←←= g2== λe.(↑e ∈b Ib2)@i
22. g2 is Q2-R-pre-preserving on λe.(↑e ∈b Ib2)@i
23. ∀a1,a2:E(Ib2). (((g2 a1) = (g2 a2) ∈ E) ⇒ (a1 = a2 ∈ E(Ib2)))@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. λe.(↑e ∈b [Ia1?Ia2]) ←←= [λe.(↑e ∈b Ib1)? g1 : g2]== λe.(↑e ∈b [Ib1?Ib2])
26. [λe.(↑e ∈b Ib1)? g1 : g2] is Q1|λe.(↑e ∈b Ia1) ∨ Q2|λe.(↑e ∈b Ia2)-R-pre-preserving on λe.(↑e ∈b [Ib1?Ib2])
27. a1 : E([Ib1?Ib2])@i
28. a2 : E([Ib1?Ib2])@i
29. y : ¬↑a1 ∈b Ib1
30. bool-decider(a1 ∈b Ib1) = (inr y ) ∈ Dec(↑a1 ∈b Ib1)
31. (g2 a1) = if p:↑a2 ∈b Ib1 then g1 a2 else g2 a2 fi ∈ E
⊢ a1 = a2 ∈ E([Ib1?Ib2])
Latex:
Latex:
1. Info : Type
2. es : EO+(Info)@i'
3. Q1 : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
4. Q2 : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
5. R : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
6. A : Type
7. B : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) {}\mrightarrow{} B@i
13. g1 : E(Ib1) {}\mrightarrow{} E(Ia1)@i
14. g2 : E(Ib2) {}\mrightarrow{} E(Ia2)@i
15. Ia1 \mcap{} Ia2 = 0
16. Ib1 \mcap{} Ib2 = 0
17. \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ia1) \mleftarrow{}\mleftarrow{}= g1== \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib1)@i
18. g1 is Q1-R-pre-preserving on \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib1)@i
19. \mforall{}a1,a2:E(Ib1). (((g1 a1) = (g1 a2)) {}\mRightarrow{} (a1 = a2))@i
20. \mforall{}e:E(Ib1). ((f (g1 e)) = Ib1(e))@i
21. \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ia2) \mleftarrow{}\mleftarrow{}= g2== \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib2)@i
22. g2 is Q2-R-pre-preserving on \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib2)@i
23. \mforall{}a1,a2:E(Ib2). (((g2 a1) = (g2 a2)) {}\mRightarrow{} (a1 = a2))@i
24. \mforall{}e:E(Ib2). ((f (g2 e)) = Ib2(e))@i
25. \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} [Ia1?Ia2]) \mleftarrow{}\mleftarrow{}= [\mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib1)? g1 : g2]== \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} [Ib1?Ib2])
26. [\mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib1)? g1 : g2] is Q1|\mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ia1)
\mvee{} Q2|\mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ia2)-R-pre-preserving on \mlambda{}e.(\muparrow{}e \mmember{}\msubb{} [Ib1?Ib2])
27. a1 : E([Ib1?Ib2])@i
28. a2 : E([Ib1?Ib2])@i
29. ([\mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib1)? g1 : g2] a1) = ([\mlambda{}e.(\muparrow{}e \mmember{}\msubb{} Ib1)? g1 : g2] a2)@i
\mvdash{} a1 = a2
By
Latex:
(RepUR ``conditional`` (-1) THEN Branch (-1))
Home
Index