Nuprl - Proof: filter swap adjacent

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

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: filter swap adjacent

A:Type, P:(A

A

Prop), f:(A

), L1,L2:A List.

(L1 swap adjacent[P(x,y)] L2)

(filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))

filter(f;L1) = filter(f;L2)

By:	Auto THEN Unfold `swap_adjacent` -1 THEN Reduce -1 THEN ExRepD THEN Inst Thm: swap adjacent decomp [A;i;L1] THEN ExRepD

Generated subgoal:

1 1. A : Type
2. P : AAProp
3. f : A
4. L1 : A List
5. L2 : A List
6. i : (||L1||-1)
7. P(L1[i],L1[(i+1)])
8. L2 = swap(L1;i;i+1)
9. X : A List
10. Y : A List
11. L1 = (X @ [L1[i]; L1[(i+1)]] @ Y)
12. swap(L1;i;i+1) = (X @ [L1[(i+1)]; L1[i]] @ Y)
(filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))
filter(f;L1) = filter(f;L2)
8 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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