---

Step * 1 1 1 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@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
19. (addp x u x)
20. x1 : T@i
21. a : T@i
22. b : T@i
23. xa : T@i
24. xb : T@i
25. (addp x1 a xa)@i
26. (addp x1 b xb)@i
27. (eq xa xb)@i
 (eq a b)
BY
{ ((InstHyp [u] 12 THEN Auto) THEN (InstHyp [x1] (-1)  THEN Auto) THEN D (-1)) }

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
19. (addp x u x)
20. x1 : T@i
21. a : T@i
22. b : T@i
23. xa : T@i
24. xb : T@i
25. (addp x1 a xa)@i
26. (addp x1 b xb)@i
27. (eq xa xb)@i
28. x:T. xi:T. ((addp x xi u))
29. xi : T
30. (addp x1 xi u)
 (eq a b)



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.  u  :  T@i
9.  \muparrow{}(zero  u)@i
10.  \mforall{}u,x:T.    ((\muparrow{}(zero  u))  {}\mRightarrow{}  ((\muparrow{}(addp  x  u  x))  \mwedge{}  (\muparrow{}(addp  u  x  x))))@i
11.  EquivRel(T;x,y.\muparrow{}(eq  x  y))@i
12.  \mforall{}u:T.  ((\muparrow{}(zero  u))  {}\mRightarrow{}  (\mforall{}x:T.  \mexists{}xi:T.  (\muparrow{}(addp  x  xi  u))))@i
13.  \mforall{}x,y:T.    ((\muparrow{}(eq  x  y))  {}\mRightarrow{}  (\muparrow{}(zero  x)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(zero  y)))@i
14.  x  :  T@i
15.  y  :  T@i
16.  z  :  T@i
17.  \muparrow{}(addp  x  y  z)@i
18.  \muparrow{}(eq  z  x)@i
19.  \muparrow{}(addp  x  u  x)
20.  x1  :  T@i
21.  a  :  T@i
22.  b  :  T@i
23.  xa  :  T@i
24.  xb  :  T@i
25.  \muparrow{}(addp  x1  a  xa)@i
26.  \muparrow{}(addp  x1  b  xb)@i
27.  \muparrow{}(eq  xa  xb)@i
\mvdash{}  \muparrow{}(eq  a  b)


By

((InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  12\mcdot{}  THEN  Auto)  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-1)  \mcdot{}  THEN  Auto)  THEN  D  (-1))



Home Index