---

Step * of Lemma isaxiom-sqequal

∀[C:Base]
  ∀[A,B,z:Base].
    if z = Ax then A z otherwise B z ~ C z 
    supposing (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax 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. (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax then a otherwise b ~ b)) ⇒ (B z ~ C z))
7. is-exception(if z = Ax then A z otherwise B z)
8. is-exception(z)
⊢ if z = Ax 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. (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax then a otherwise b ~ b)) ⇒ (B z ~ C z))
7. is-exception(C z)
8. (C)↓
⊢ C z ≤ if z = Ax then A z otherwise B z

3
1. C : Base
2. strict(C)
3. A : Base
4. B : Base
5. z : Base
6. (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax then a otherwise b ~ b)) ⇒ (B z ~ C z))
7. is-exception(C z)
8. is-exception(C)
⊢ C z ≤ if z = Ax then A z otherwise B z

---

Latex:

---

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