---

Step * 1 of Lemma ispair-sqequal


1. C : Base
2. strict(C)
3. A : Base
4. B : Base
5. z : Base
6. ((z ~ <fst(z), snd(z)>) ⇒ (A <fst(z), snd(z)> ~ C <fst(z), snd(z)>))
∧ ((∀a,b:Base.  (if z is a pair then a otherwise b ~ b)) ⇒ (B z ~ C z))
7. is-exception(if z is a pair then A z otherwise B z)
8. is-exception(z)
⊢ if z is a pair then A z otherwise B z ≤ C z
BY
{ (ExceptionSqequal (-1) THEN HypSubst' (-1) 0 THEN RW (AddrC [1] (TagC (mk_tag_term 1))) 0) }

1
1. C : Base
2. strict(C)
3. A : Base
4. B : Base
5. z : Base
6. ((z ~ <fst(z), snd(z)>) ⇒ (A <fst(z), snd(z)> ~ C <fst(z), snd(z)>))
∧ ((∀a,b:Base.  (if z is a pair then a otherwise b ~ b)) ⇒ (B z ~ C z))
7. is-exception(if z is a pair then A z otherwise B z)
8. is-exception(z)
9. u : Base
10. v : Base
11. z ~ exception(u; v)
⊢ exception(u; v) ≤ C (exception(u; v))

---

Latex:

---

Latex:

1.  C  :  Base
2.  strict(C)
3.  A  :  Base
4.  B  :  Base
5.  z  :  Base
6.  ((z  \msim{}  <fst(z),  snd(z)>)  {}\mRightarrow{}  (A  <fst(z),  snd(z)>  \msim{}  C  <fst(z),  snd(z)>))
\mwedge{}  ((\mforall{}a,b:Base.    (if  z  is  a  pair  then  a  otherwise  b  \msim{}  b))  {}\mRightarrow{}  (B  z  \msim{}  C  z))
7.  is-exception(if  z  is  a  pair  then  A  z  otherwise  B  z)
8.  is-exception(z)
\mvdash{}  if  z  is  a  pair  then  A  z  otherwise  B  z  \mleq{}  C  z


By

---

Latex:
(ExceptionSqequal  (-1)  THEN  HypSubst'  (-1)  0  THEN  RW  (AddrC  [1]  (TagC  (mk\_tag\_term  1)))  0)

---

Home Index