---

Step * of Lemma ispair-sqequal

∀[C:Base]
  ∀[A,B,z:Base].
    if z is a pair then A z otherwise B z ~ C z 
    supposing ((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)) 
  supposing strict(C)
BY
{ (SqReasoning
   THEN Try (Complete ((SplitAndHyps THEN (HVimplies2 0 [1] ORELSE HVimplies2 0 [2]) THEN RWO "6" 0 THEN Auto)))
   ) }

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)
⊢ if z is a pair then A z otherwise B z ≤ C z

2
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(C z)
8. (C)↓
⊢ C z ≤ if z is a pair then A z otherwise B z

3
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(C z)
8. is-exception(C)
⊢ C z ≤ if z is a pair then A z otherwise B z

---

Latex:

---

Latex:
\mforall{}[C:Base]
    \mforall{}[A,B,z:Base].
        if  z  is  a  pair  then  A  z  otherwise  B  z  \msim{}  C  z 
        supposing  ((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)) 
    supposing  strict(C)


By

---

Latex:
(SqReasoning
  THEN  Try  (Complete  ((SplitAndHyps
                                            THEN  (HVimplies2  0  [1]  ORELSE  HVimplies2  0  [2])
                                            THEN  RWO  "6"  0
                                            THEN  Auto)))
  )

---

Home Index