Nuprl - Proof: ring-list 1 1 2 2 2 2 3 1 1 1 2 1 2 1 1

(42steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ring-list 1 1 2 2 2 2 3 1 1 1 2 1 2 1 1

1. R : Id

2. in : |R|

IdLnk
3. out : |R|

IdLnk
4.

i:|R|.
4. R(source(in(i))) & R(destination(out(i)))
4. & source(out(i)) = i
4. & & destination(in(i)) = i
4. & & in(destination(out(i))) = out(i)
4. & & out(source(in(i))) = in(i)
5.

i,j:|R|.

x.destination(out(x))^k(i) = j
6. i : |R|
7. k :

x.destination(out(x))^k(i) = i
9. (

x.destination(out(x)))

|R|

|R|
10. i@0 : |R|
11.

i@0 = i
12. j : |R|
13. n :

14.

n1:

.
14. n1<n
14.

14.

x.destination(out(x))^n1(i) = j

(

x.destination(out(x))^m(i) = j)
15.

x.destination(out(x))^n-k(

x.destination(out(x))^k(i)) = j
16.

n<k

x.destination(out(x))^n-k(i)

x.destination(out(x))^n-k(

x.destination(out(x))^k(i))

By:	MoveToConcl 8 THEN GenConcl ((x.destination(out(x))) = f)

Generated subgoals:

1 8. (x.destination(out(x)))  |R||R|
9. i@0 : |R|
10. i@0 = i  Id
11. j : |R|
12. n :
13. n1:.
13. n1<n
13.
13. x.destination(out(x))^n1(i) = j  Id
13.
13. (m:k. x.destination(out(x))^m(i) = j  Id)
14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j  Id
15. n<k
16. f : |R||R|
17. (x.destination(out(x))) = f
18. f^k(i) = i  Id
  f^n-k(i) = f^n-k(f^k(i))  Id
7 steps

2 8. (x.destination(out(x)))  |R||R|
9. i@0 : |R|
10. i@0 = i  Id
11. j : |R|
12. n :
13. n1:.
13. n1<n
13.
13. x.destination(out(x))^n1(i) = j  Id
13.
13. (m:k. x.destination(out(x))^m(i) = j  Id)
14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j  Id
15. n<k
16. f : |R||R|
17. (x.destination(out(x))) = f
  f^k(i)  Id
1 step

3 8. (x.destination(out(x)))  |R||R|
9. i@0 : |R|
10. i@0 = i  Id
11. j : |R|
12. n :
13. n1:.
13. n1<n
13.
13. x.destination(out(x))^n1(i) = j  Id
13.
13. (m:k. x.destination(out(x))^m(i) = j  Id)
14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j  Id
15. n<k
16. f : |R||R|
17. (x.destination(out(x))) = f
  i  Id
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(42steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc

1	8. (x.destination(out(x))) \|R\|\|R\| 9. i@0 : \|R\| 10. i@0 = i Id 11. j : \|R\| 12. n : 13. n1:. 13. n1<n 13. 13. x.destination(out(x))^n1(i) = j Id 13. 13. (m:k. x.destination(out(x))^m(i) = j Id) 14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j Id 15. n<k 16. f : \|R\|\|R\| 17. (x.destination(out(x))) = f 18. f^k(i) = i Id f^n-k(i) = f^n-k(f^k(i)) Id	7 steps
2	8. (x.destination(out(x))) \|R\|\|R\| 9. i@0 : \|R\| 10. i@0 = i Id 11. j : \|R\| 12. n : 13. n1:. 13. n1<n 13. 13. x.destination(out(x))^n1(i) = j Id 13. 13. (m:k. x.destination(out(x))^m(i) = j Id) 14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j Id 15. n<k 16. f : \|R\|\|R\| 17. (x.destination(out(x))) = f f^k(i) Id	1 step
3	8. (x.destination(out(x))) \|R\|\|R\| 9. i@0 : \|R\| 10. i@0 = i Id 11. j : \|R\| 12. n : 13. n1:. 13. n1<n 13. 13. x.destination(out(x))^n1(i) = j Id 13. 13. (m:k. x.destination(out(x))^m(i) = j Id) 14. x.destination(out(x))^n-k(x.destination(out(x))^k(i)) = j Id 15. n<k 16. f : \|R\|\|R\| 17. (x.destination(out(x))) = f i Id	1 step