Step
*
1
3
1
1
2
3
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@i
29. ↑a2 ∈b Ib2
30. x : ↑a1 ∈b Ib1
31. bool-decider(a1 ∈b Ib1) = (inl x) ∈ Dec(↑a1 ∈b Ib1)
32. y : ¬↑a2 ∈b Ib1
33. bool-decider(a2 ∈b Ib1) = (inr y ) ∈ Dec(↑a2 ∈b Ib1)
34. (g1 a1) = (g2 a2) ∈ E
⊢ False
BY
{ OnMaybeHyp 15 (\h. (((Unfold `es-interface-disjoint` h THEN (InstHyp [⌈es⌉;⌈g1 a1⌉] h)⋅) THENA Auto)
                      THEN D -1
                      THEN D 0))⋅ }
1
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. ∀es:EO+(Info). ∀e:E.  (¬((↑e ∈b Ia1) ∧ (↑e ∈b Ia2)))
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@i
29. ↑a2 ∈b Ib2
30. x : ↑a1 ∈b Ib1
31. bool-decider(a1 ∈b Ib1) = (inl x) ∈ Dec(↑a1 ∈b Ib1)
32. y : ¬↑a2 ∈b Ib1
33. bool-decider(a2 ∈b Ib1) = (inr y ) ∈ Dec(↑a2 ∈b Ib1)
34. (g1 a1) = (g2 a2) ∈ E
⊢ ↑g1 a1 ∈b Ia1
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. ∀es:EO+(Info). ∀e:E.  (¬((↑e ∈b Ia1) ∧ (↑e ∈b Ia2)))
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@i
29. ↑a2 ∈b Ib2
30. x : ↑a1 ∈b Ib1
31. bool-decider(a1 ∈b Ib1) = (inl x) ∈ Dec(↑a1 ∈b Ib1)
32. y : ¬↑a2 ∈b Ib1
33. bool-decider(a2 ∈b Ib1) = (inr y ) ∈ Dec(↑a2 ∈b Ib1)
34. (g1 a1) = (g2 a2) ∈ E
⊢ ↑g1 a1 ∈b Ia2
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@i
29.  \muparrow{}a2  \mmember{}\msubb{}  Ib2
30.  x  :  \muparrow{}a1  \mmember{}\msubb{}  Ib1
31.  bool-decider(a1  \mmember{}\msubb{}  Ib1)  =  (inl  x)
32.  y  :  \mneg{}\muparrow{}a2  \mmember{}\msubb{}  Ib1
33.  bool-decider(a2  \mmember{}\msubb{}  Ib1)  =  (inr  y  )
34.  (g1  a1)  =  (g2  a2)
\mvdash{}  False
By
Latex:
OnMaybeHyp  15  (\mbackslash{}h.  (((Unfold  `es-interface-disjoint`  h  THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}g1  a1\mkleeneclose{}]  h)\mcdot{})  THENA  Auto)
                                        THEN  D  -1
                                        THEN  D  0))\mcdot{}
Home
Index