---

Step * 2 1 1 of Lemma ispair-sqequal


1. C : Base
2. ∀x:Base. ((C x)↓ ⇒ (x)↓)
3. ∀u,v:Base.  (C (exception(u; v)) ~ exception(u; v))
4. ∀z:Base. (is-exception(C z) ⇒ is-exception(z))
5. A : Base
6. B : Base
7. z : Base
8. (z ~ <fst(z), snd(z)>) ⇒ (A <fst(z), snd(z)> ~ C <fst(z), snd(z)>)
9. (∀a,b:Base.  (if z is a pair then a otherwise b ~ b)) ⇒ (B z ~ C z)
10. is-exception(C z)
11. (C)↓
12. is-exception(z)
13. u : Base
14. v : Base
15. z ~ exception(u; v)
⊢ C (exception(u; v)) ≤ if exception(u; v) is a pair then A (exception(u; v)) otherwise B (exception(u; v))
BY
{ ((RWO "3" 0 THENA Auto) THEN RW  (AddrC [2] (TagC (mk_tag_term 1))) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Base
2.  \mforall{}x:Base.  ((C  x)\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{})
3.  \mforall{}u,v:Base.    (C  (exception(u;  v))  \msim{}  exception(u;  v))
4.  \mforall{}z:Base.  (is-exception(C  z)  {}\mRightarrow{}  is-exception(z))
5.  A  :  Base
6.  B  :  Base
7.  z  :  Base
8.  (z  \msim{}  <fst(z),  snd(z)>)  {}\mRightarrow{}  (A  <fst(z),  snd(z)>  \msim{}  C  <fst(z),  snd(z)>)
9.  (\mforall{}a,b:Base.    (if  z  is  a  pair  then  a  otherwise  b  \msim{}  b))  {}\mRightarrow{}  (B  z  \msim{}  C  z)
10.  is-exception(C  z)
11.  (C)\mdownarrow{}
12.  is-exception(z)
13.  u  :  Base
14.  v  :  Base
15.  z  \msim{}  exception(u;  v)
\mvdash{}  C  (exception(u;  v))  \mleq{}  if  exception(u;  v)  is  a  pair  then  A  (exception(u;  v))
                                                otherwise  B  (exception(u;  v))


By

---

Latex:
((RWO  "3"  0  THENA  Auto)  THEN  RW    (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  0  THEN  Auto)

---

Home Index