---

Step * 1 of Lemma Q-R-glued-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. Ia1 ∩ Ia2 = 0
14. Ib1 ∩ Ib2 = 0
15. g1 : E(Ib1) ─→ E@i
16. g1 glues Ia1:Q1 ──f─→ Ib1:R@i
17. g : E(Ib2) ─→ E@i
18. g glues Ia2:Q2 ──f─→ Ib2:R@i
19. [Ia1?Ia2] ∈ EClass(A)
20. E(Ia1) ⊆r E([Ia1?Ia2])
21. g ∈ E(Ib2) ─→ E(Ia2)
22. g1 ∈ E(Ib1) ─→ E(Ia1)
⊢ ∃g:E([Ib1?Ib2]) ─→ E. g glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R
BY
{ ((InstConcl [⌈[{Ib1}? g1 : g]⌉])⋅
   THENA (Try ((((InstLemma `conditional_wf-interface2` [Info; ⌈es⌉; ⌈A⌉; ⌈B⌉; ⌈Ia1⌉; ⌈Ia2⌉; ⌈Ib1⌉; ⌈Ib2⌉; ⌈g1⌉; ⌈g⌉])⋅
                 THENA Auto
                 )
                THEN (es_pred_rewrite (-1))
                THEN (Fold `es-interface-predicate` (-1))
                THEN Trivial))
          THEN Auto
          THEN BLemma `es-interface-conditional`
          THEN Auto)
   ) }

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. Ia1 ∩ Ia2 = 0
14. Ib1 ∩ Ib2 = 0
15. g1 : E(Ib1) ─→ E@i
16. g1 glues Ia1:Q1 ──f─→ Ib1:R@i
17. g : E(Ib2) ─→ E@i
18. g glues Ia2:Q2 ──f─→ Ib2:R@i
19. [Ia1?Ia2] ∈ EClass(A)
20. E(Ia1) ⊆r E([Ia1?Ia2])
21. g ∈ E(Ib2) ─→ E(Ia2)
22. g1 ∈ E(Ib1) ─→ E(Ia1)
⊢ [{Ib1}? g1 : g] glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R

---

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.  Ia1  \mcap{}  Ia2  =  0
14.  Ib1  \mcap{}  Ib2  =  0
15.  g1  :  E(Ib1)  {}\mrightarrow{}  E@i
16.  g1  glues  Ia1:Q1  {}{}f{}\mrightarrow{}  Ib1:R@i
17.  g  :  E(Ib2)  {}\mrightarrow{}  E@i
18.  g  glues  Ia2:Q2  {}{}f{}\mrightarrow{}  Ib2:R@i
19.  [Ia1?Ia2]  \mmember{}  EClass(A)
20.  E(Ia1)  \msubseteq{}r  E([Ia1?Ia2])
21.  g  \mmember{}  E(Ib2)  {}\mrightarrow{}  E(Ia2)
22.  g1  \mmember{}  E(Ib1)  {}\mrightarrow{}  E(Ia1)
\mvdash{}  \mexists{}g:E([Ib1?Ib2])  {}\mrightarrow{}  E.  g  glues  [Ia1?Ia2]:Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}  {}{}f{}\mrightarrow{}  [Ib1?Ib2]:R


By

---

Latex:
((InstConcl  [\mkleeneopen{}[\{Ib1\}?  g1  :  g]\mkleeneclose{}])\mcdot{}
  THENA  (Try  ((((InstLemma  `conditional\_wf-interface2`  [Info;  \mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}Ia1\mkleeneclose{};  \mkleeneopen{}Ia2\mkleeneclose{};  \mkleeneopen{}Ib1\mkleeneclose{}; 
                              \mkleeneopen{}Ib2\mkleeneclose{};  \mkleeneopen{}g1\mkleeneclose{};  \mkleeneopen{}g\mkleeneclose{}])\mcdot{}
                              THENA  Auto
                              )
                            THEN  (es\_pred\_rewrite  (-1))
                            THEN  (Fold  `es-interface-predicate`  (-1))
                            THEN  Trivial))
                THEN  Auto
                THEN  BLemma  `es-interface-conditional`
                THEN  Auto)
  )

---

Home Index