(27steps 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: swap adjacent decomp
  A:Type, i:, L:A List.
  i+1<||L||
  
  (X,Y:A List.
  (L = (X @ [L[i]; L[(i+1)]] @ Y) & swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))
By: InductionOnNat

Generated subgoals:

1 1. A : Type
  L:A List. 
  0+1<||L||
  
  (X,Y:A List.
  (L = (X @ [L[0]; L[(0+1)]] @ Y) & swap(L;0;0+1) = (X @ [L[(0+1)]; L[0]] @ Y))
19 steps
2 1. A : Type
2. i : 
3. 0<i
4. L:A List. 
4. i-1+1<||L||
4. 
4. (X,Y:A List.
4. (L = (X @ [L[(i-1)]; L[(i-1+1)]] @ Y)
4. (& swap(L;i-1;i-1+1) = (X @ [L[(i-1+1)]; L[(i-1)]] @ Y))
  L:A List. 
  i+1<||L||
  
  (X,Y:A List.
  (L = (X @ [L[i]; L[(i+1)]] @ Y) & swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))
7 steps

About:
listconsnilnatural_numberaddless_thanuniverse
equalimpliesandallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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