---

Step * of Lemma hw5_7_2

T:Type. eq:T  T  . addp:T  T  T  . zero:T  .
  (((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))))))
   (x,y,z,t1,t2,r:T.  ((((addp x y t1))  ((addp t1 z r))  ((addp y z t2)))  ((addp t2 x r))))
   (x,y,z:T.  (((addp x y z))  ((addp y x z))))
   ((u:T. ((zero u)))  (u,x:T.  (((zero u))  (((addp x u x))  ((addp u x x))))))
   EquivRel(T;x,y.(eq x y))
   (u:T. (((zero u))  (x:T. xi:T. ((addp x xi u)))))
   (x,y:T.  (((eq x y))  ((zero x)  (zero y)))))
   (x,y,z:T.  ((((addp x y z))  ((eq z x)))  ((zero y)))))
BY
{ Auto }

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. ((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)


\mforall{}T:Type.  \mforall{}eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}addp:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}zero:T  {}\mrightarrow{}  \mBbbB{}.
    (((\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))))))
    \mwedge{}  (\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))))
    \mwedge{}  (\mforall{}x,y,z:T.    ((\muparrow{}(addp  x  y  z))  {}\mRightarrow{}  (\muparrow{}(addp  y  x  z))))
    \mwedge{}  ((\mexists{}u:T.  (\muparrow{}(zero  u)))  \mwedge{}  (\mforall{}u,x:T.    ((\muparrow{}(zero  u))  {}\mRightarrow{}  ((\muparrow{}(addp  x  u  x))  \mwedge{}  (\muparrow{}(addp  u  x  x))))))
    \mwedge{}  EquivRel(T;x,y.\muparrow{}(eq  x  y))
    \mwedge{}  (\mforall{}u:T.  ((\muparrow{}(zero  u))  {}\mRightarrow{}  (\mforall{}x:T.  \mexists{}xi:T.  (\muparrow{}(addp  x  xi  u)))))
    \mwedge{}  (\mforall{}x,y:T.    ((\muparrow{}(eq  x  y))  {}\mRightarrow{}  (\muparrow{}(zero  x)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(zero  y)))))
    {}\mRightarrow{}  (\mforall{}x,y,z:T.    (((\muparrow{}(addp  x  y  z))  \mwedge{}  (\muparrow{}(eq  z  x)))  {}\mRightarrow{}  (\muparrow{}(zero  y)))))


By

Auto



Home Index