---

Step * 1 of Lemma conditional_wf-interface


1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. Ia1 : EClass(A)
6. Ia2 : EClass(A)
7. Ib1 : EClass(B)
8. Ib2 : EClass(B)
9. g1 : E(Ib1) ─→ E(Ia1)
10. g2 : E(Ib2) ─→ E(Ia2)
⊢ λx.if p:{Ib1} x then g1 x else g2 x fi  ∈ E([Ib1?Ib2]) ─→ E([Ia1?Ia2])
BY
{ (RepUR ``es-interface-predicate`` 0 THEN RepeatFor 3 (MemCD) THEN Try (CompleteAuto)) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. Ia1 : EClass(A)
6. Ia2 : EClass(A)
7. Ib1 : EClass(B)
8. Ib2 : EClass(B)
9. g1 : E(Ib1) ─→ E(Ia1)
10. g2 : E(Ib2) ─→ E(Ia2)
11. x : E([Ib1?Ib2])@i
12. q : ¬↑x ∈b Ib1
⊢ g2 x ∈ E([Ia1?Ia2])

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  B  :  Type
5.  Ia1  :  EClass(A)
6.  Ia2  :  EClass(A)
7.  Ib1  :  EClass(B)
8.  Ib2  :  EClass(B)
9.  g1  :  E(Ib1)  {}\mrightarrow{}  E(Ia1)
10.  g2  :  E(Ib2)  {}\mrightarrow{}  E(Ia2)
\mvdash{}  \mlambda{}x.if  p:\{Ib1\}  x  then  g1  x  else  g2  x  fi    \mmember{}  E([Ib1?Ib2])  {}\mrightarrow{}  E([Ia1?Ia2])


By

---

Latex:
(RepUR  ``es-interface-predicate``  0  THEN  RepeatFor  3  (MemCD)  THEN  Try  (CompleteAuto))

---

Home Index