Nuprl - Proof: symmetric swap adjacent

(2steps 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: symmetric swap adjacent

A:Type, P:(A

A

Prop).

(Sym x,y:A. P(x,y))

(Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)

By:	Unfolds [`sym`;`swap_adjacent`] 0 THEN Reduce 0 THEN ParallelOp -1 THEN ExRepD THEN FwdThru Thm: swapped select [-1]

Generated subgoal:

1 1. A : Type
2. P : AAProp
3. a,b:A. P(a,b)  P(b,a)
4. a : A List
5. b : A List
6. i : (||a||-1)
7. P(a[i],a[(i+1)])
8. b = swap(a;i;i+1)
9. b[i] = a[(i+1)]
10. b[(i+1)] = a[i]
11. ||b|| = ||a||
12. a = swap(b;i;i+1)
13. x:||b||. x = i  x = i+1  b[x] = a[x]
  P(b[i],b[(i+1)])
1 step

About:

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

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