---

Step * 1 2 1 1 1 1 2 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. {Ia1} ←←= g1== {Ib1}@i
18. g1 is Q1-R-pre-preserving on {Ib1}@i
19. Inj(E(Ib1);E;g1)@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. {Ia2} ←←= g2== {Ib2}@i
22. g2 is Q2-R-pre-preserving on {Ib2}@i
23. Inj(E(Ib2);E;g2)@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. {[Ia1?Ia2]} ←←= [{Ib1}? g1 : g2]== {[Ib1?Ib2]}
26. [{Ib1}? g1 : g2] ∈ E([Ib1?Ib2]) ─→ E([Ia1?Ia2])
27. R ∨ R ⇐⇒ R
28. [{Ib1}? g1 : g2] ∈ {e:E| ({Ib1} ∨ {Ib2}) e}  ─→ {e:E| {[Ia1?Ia2]} e} 
⊢ [{Ib1}? g1 : g2] is Q1|{Ia1} ∨ Q2|{Ia2}-R ∨ R-pre-preserving on {Ib1} ∨ {Ib2}
BY
{ ((Assert g1 ∈ {e:E| {Ib1} e}  ─→ E BY
          ((UnivCD THENA Auto)
           THEN D 0
           THEN Auto
           THEN (RepUR ``rel-restriction es-interface-predicate`` (-1))⋅
           THEN (Assert g1 e ∈ E(Ia1) BY
                       Auto)
           THEN OnMaybeHyp 15 (\h. (Unfold `es-interface-disjoint` h
                                    THEN ((InstHyp [⌈es⌉;⌈g1 e⌉] h)⋅ THENA Auto)
                                    THEN D (-1)
                                    THEN CompleteAuto))⋅))
   THEN (Assert g2 ∈ {e:E| {Ib2} e}  ─→ E BY
               ((UnivCD THENA Auto)
                THEN D 0
                THEN Auto
                THEN (RepUR ``rel-restriction es-interface-predicate`` (-1))⋅
                THEN (Assert g2 e ∈ E(Ia2) BY
                            Auto)
                THEN OnMaybeHyp 15 (\h. (Unfold `es-interface-disjoint` h
                                         THEN ((InstHyp [⌈es⌉;⌈g2 e⌉] h)⋅ THENA Auto)
                                         THEN D (-1)
                                         THEN CompleteAuto))⋅))
   ) }

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. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. {Ia1} ←←= g1== {Ib1}@i
18. g1 is Q1-R-pre-preserving on {Ib1}@i
19. Inj(E(Ib1);E;g1)@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. {Ia2} ←←= g2== {Ib2}@i
22. g2 is Q2-R-pre-preserving on {Ib2}@i
23. Inj(E(Ib2);E;g2)@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. {[Ia1?Ia2]} ←←= [{Ib1}? g1 : g2]== {[Ib1?Ib2]}
26. [{Ib1}? g1 : g2] ∈ E([Ib1?Ib2]) ─→ E([Ia1?Ia2])
27. R ∨ R ⇐⇒ R
28. [{Ib1}? g1 : g2] ∈ {e:E| ({Ib1} ∨ {Ib2}) e}  ─→ {e:E| {[Ia1?Ia2]} e} 
29. g1 ∈ {e:E| {Ib1} e}  ─→ E
30. g2 ∈ {e:E| {Ib2} e}  ─→ E
⊢ [{Ib1}? g1 : g2] is Q1|{Ia1} ∨ Q2|{Ia2}-R ∨ R-pre-preserving on {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.  \{Ia1\}  \mleftarrow{}\mleftarrow{}=  g1==  \{Ib1\}@i
18.  g1  is  Q1-R-pre-preserving  on  \{Ib1\}@i
19.  Inj(E(Ib1);E;g1)@i
20.  \mforall{}e:E(Ib1).  ((f  (g1  e))  =  Ib1(e))@i
21.  \{Ia2\}  \mleftarrow{}\mleftarrow{}=  g2==  \{Ib2\}@i
22.  g2  is  Q2-R-pre-preserving  on  \{Ib2\}@i
23.  Inj(E(Ib2);E;g2)@i
24.  \mforall{}e:E(Ib2).  ((f  (g2  e))  =  Ib2(e))@i
25.  \{[Ia1?Ia2]\}  \mleftarrow{}\mleftarrow{}=  [\{Ib1\}?  g1  :  g2]==  \{[Ib1?Ib2]\}
26.  [\{Ib1\}?  g1  :  g2]  \mmember{}  E([Ib1?Ib2])  {}\mrightarrow{}  E([Ia1?Ia2])
27.  R  \mvee{}  R  \mLeftarrow{}{}\mRightarrow{}  R
28.  [\{Ib1\}?  g1  :  g2]  \mmember{}  \{e:E|  (\{Ib1\}  \mvee{}  \{Ib2\})  e\}    {}\mrightarrow{}  \{e:E|  \{[Ia1?Ia2]\}  e\} 
\mvdash{}  [\{Ib1\}?  g1  :  g2]  is  Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}-R  \mvee{}  R-pre-preserving  on  \{Ib1\}  \mvee{}  \{Ib2\}


By

---

Latex:
((Assert  g1  \mmember{}  \{e:E|  \{Ib1\}  e\}    {}\mrightarrow{}  E  BY
                ((UnivCD  THENA  Auto)
                  THEN  D  0
                  THEN  Auto
                  THEN  (RepUR  ``rel-restriction  es-interface-predicate``  (-1))\mcdot{}
                  THEN  (Assert  g1  e  \mmember{}  E(Ia1)  BY
                                          Auto)
                  THEN  OnMaybeHyp  15  (\mbackslash{}h.  (Unfold  `es-interface-disjoint`  h
                                                                    THEN  ((InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}g1  e\mkleeneclose{}]  h)\mcdot{}  THENA  Auto)
                                                                    THEN  D  (-1)
                                                                    THEN  CompleteAuto))\mcdot{}))
  THEN  (Assert  g2  \mmember{}  \{e:E|  \{Ib2\}  e\}    {}\mrightarrow{}  E  BY
                          ((UnivCD  THENA  Auto)
                            THEN  D  0
                            THEN  Auto
                            THEN  (RepUR  ``rel-restriction  es-interface-predicate``  (-1))\mcdot{}
                            THEN  (Assert  g2  e  \mmember{}  E(Ia2)  BY
                                                    Auto)
                            THEN  OnMaybeHyp  15  (\mbackslash{}h.  (Unfold  `es-interface-disjoint`  h
                                                                              THEN  ((InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}g2  e\mkleeneclose{}]  h)\mcdot{}  THENA  Auto)
                                                                              THEN  D  (-1)
                                                                              THEN  CompleteAuto))\mcdot{}))
  )

---

Home Index