Step
*
1
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
28. x:T. xi:T. ((addp x xi u))
29. xi : T
30. (addp x1 xi u)
(eq a b)
BY
{ ((Assert (addp xa xi a) BY
(InstHyp [
xi
;x1;a;u;xa;a] 6
THEN Auto))
THEN (Assert (addp xb xi b) BY
(InstHyp [xi;x1;b;u;xb;b] 6 THEN 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@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)
31. (addp xa xi a)
32. (addp xb xi b)
(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
28. \mforall{}x:T. \mexists{}xi:T. (\muparrow{}(addp x xi u))
29. xi : T
30. \muparrow{}(addp x1 xi u)
\mvdash{} \muparrow{}(eq a b)
By
((Assert \muparrow{}(addp xa xi a) BY
(InstHyp [\mkleeneopen{}xi\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}xa\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}] 6\mcdot{} THEN Auto))
THEN (Assert \muparrow{}(addp xb xi b) BY
(InstHyp [\mkleeneopen{}xi\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}xb\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}] 6\mcdot{} THEN Auto))
)
Home
Index