---

Step * 1 of Lemma hw5_7_2


1. T : Type@i'
2. eq : T  T  @i
3. addp : T  T  T  @i
4. zero : T  @i
5. x,y:T.
     ((z:T. ((addp x y z)))
      (xp,yp,zp,z:T.  ((((eq x xp))  ((eq y yp))  ((addp xp yp zp))  ((addp x y z)))  ((eq z zp)))))@i
6. x,y,z,t1,t2,r:T.  ((((addp x y t1))  ((addp t1 z r))  ((addp y z t2)))  ((addp t2 x r)))@i
7. x,y,z:T.  (((addp x y z))  ((addp y x z)))@i
8. u:T. ((zero u))@i
9. u,x:T.  (((zero u))  (((addp x u x))  ((addp u x x))))@i
10. EquivRel(T;x,y.(eq x y))@i
11. u:T. (((zero u))  (x:T. xi:T. ((addp x xi u))))@i
12. x,y:T.  (((eq x y))  ((zero x)  (zero y)))@i
13. x : T@i
14. y : T@i
15. z : T@i
16. (addp x y z)@i
17. (eq z x)@i
 (zero y)
BY
{ (D (8) THEN skip{get the identity element}) }

1
1. T : Type@i'
2. eq : T  T  @i
3. addp : T  T  T  @i
4. zero : T  @i
5. x,y:T.
     ((z:T. ((addp x y z)))
      (xp,yp,zp,z:T.  ((((eq x xp))  ((eq y yp))  ((addp xp yp zp))  ((addp x y z)))  ((eq z zp)))))@i
6. x,y,z,t1,t2,r:T.  ((((addp x y t1))  ((addp t1 z r))  ((addp y z t2)))  ((addp t2 x r)))@i
7. x,y,z:T.  (((addp x y z))  ((addp y x z)))@i
8. u : T@i
9. (zero u)@i
10. u,x:T.  (((zero u))  (((addp x u x))  ((addp u x x))))@i
11. EquivRel(T;x,y.(eq x y))@i
12. u:T. (((zero u))  (x:T. xi:T. ((addp x xi u))))@i
13. x,y:T.  (((eq x y))  ((zero x)  (zero y)))@i
14. x : T@i
15. y : T@i
16. z : T@i
17. (addp x y z)@i
18. (eq z x)@i
 (zero y)



1.  T  :  Type@i'
2.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}@i
3.  addp  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}@i
4.  zero  :  T  {}\mrightarrow{}  \mBbbB{}@i
5.  \mforall{}x,y:T.
          ((\mexists{}z:T.  (\muparrow{}(addp  x  y  z)))
          \mwedge{}  (\mforall{}xp,yp,zp,z:T.
                    (((\muparrow{}(eq  x  xp))  \mwedge{}  (\muparrow{}(eq  y  yp))  \mwedge{}  (\muparrow{}(addp  xp  yp  zp))  \mwedge{}  (\muparrow{}(addp  x  y  z)))  {}\mRightarrow{}  (\muparrow{}(eq  z  zp)))))@i
6.  \mforall{}x,y,z,t1,t2,r:T.
          (((\muparrow{}(addp  x  y  t1))  \mwedge{}  (\muparrow{}(addp  t1  z  r))  \mwedge{}  (\muparrow{}(addp  y  z  t2)))  {}\mRightarrow{}  (\muparrow{}(addp  t2  x  r)))@i
7.  \mforall{}x,y,z:T.    ((\muparrow{}(addp  x  y  z))  {}\mRightarrow{}  (\muparrow{}(addp  y  x  z)))@i
8.  \mexists{}u:T.  (\muparrow{}(zero  u))@i
9.  \mforall{}u,x:T.    ((\muparrow{}(zero  u))  {}\mRightarrow{}  ((\muparrow{}(addp  x  u  x))  \mwedge{}  (\muparrow{}(addp  u  x  x))))@i
10.  EquivRel(T;x,y.\muparrow{}(eq  x  y))@i
11.  \mforall{}u:T.  ((\muparrow{}(zero  u))  {}\mRightarrow{}  (\mforall{}x:T.  \mexists{}xi:T.  (\muparrow{}(addp  x  xi  u))))@i
12.  \mforall{}x,y:T.    ((\muparrow{}(eq  x  y))  {}\mRightarrow{}  (\muparrow{}(zero  x)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(zero  y)))@i
13.  x  :  T@i
14.  y  :  T@i
15.  z  :  T@i
16.  \muparrow{}(addp  x  y  z)@i
17.  \muparrow{}(eq  z  x)@i
\mvdash{}  \muparrow{}(zero  y)


By

(D  (8)  THEN  skip\{get  the  identity  element\})



Home Index