Nuprl - Proof: permute by flips

(31steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: permute by flips

, p:(

k). Bij(

k; p)

(

(k-1) List. p = compose_flips(L))

By:	Analyze 0 THEN NatInd 1

Generated subgoals:

1 1. p : 00
2. Bij(0; 0; p)
  L:(0-1) List. p = compose_flips(L)
2 steps

2 1. k :
2. 0<k
3. p:((k-1)(k-1)).
3. Bij((k-1); (k-1); p)  (L:(k-1-1) List. p = compose_flips(L))
4. p : kk
5. Bij(k; k; p)
  L:(k-1) List. p = compose_flips(L)
28 steps

About:

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

(31steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

1	1. p : 00 2. Bij(0; 0; p) L:(0-1) List. p = compose_flips(L)	2 steps
2	1. k : 2. 0<k 3. p:((k-1)(k-1)). 3. Bij((k-1); (k-1); p) (L:(k-1-1) List. p = compose_flips(L)) 4. p : kk 5. Bij(k; k; p) L:(k-1) List. p = compose_flips(L)	28 steps