Nuprl - Proof: lpath-members-connected 1 2 3 1 1

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

1. p : IdLnk List
2. i :

||p||
3. j :

(i+1)
4.

(||p||-1).
4. destination(p[i]) = source(p[(i+1)]) &

p[(i+1)] = lnk-inv(p[i])
5.

i-j = 0
6. destination(p[(i-1)]) = source(p[(i-1+1)])
7.

p[(i-1+1)] = lnk-inv(p[(i-1)])

source(p[i]) = destination(p[(i-1)])

By:	Symmetry THEN NthHypEq -2 THEN Analyze

Generated subgoals:

None

About:

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