Step * 2 1 of Lemma isaxiom-sqequal


1. 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. Base
6. Base
7. Base
8. Ax Ax
9. (∀a,b:Base.  (if Ax then otherwise b))  (B z)
10. is-exception(C z)
11. (C)↓
⊢ z ≤ if Ax then otherwise z
BY
((FHyp [-2] THENA Auto) THEN ExceptionSqequal (-1) THEN HypSubst' (-1) 0) }

1
1. 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. Base
6. Base
7. Base
8. Ax Ax
9. (∀a,b:Base.  (if Ax then otherwise b))  (B z)
10. is-exception(C z)
11. (C)↓
12. is-exception(z)
13. Base
14. Base
15. exception(u; v)
⊢ (exception(u; v)) ≤ if exception(u; v) Ax then (exception(u; v)) otherwise (exception(u; v))


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.  A  Ax  \msim{}  C  Ax
9.  (\mforall{}a,b:Base.    (if  z  =  Ax  then  a  otherwise  b  \msim{}  b))  {}\mRightarrow{}  (B  z  \msim{}  C  z)
10.  is-exception(C  z)
11.  (C)\mdownarrow{}
\mvdash{}  C  z  \mleq{}  if  z  =  Ax  then  A  z  otherwise  B  z


By


Latex:
((FHyp  4  [-2]  THENA  Auto)  THEN  ExceptionSqequal  (-1)  THEN  HypSubst'  (-1)  0)




Home Index