Nuprl - Pf P_no_dup

(3steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

E:EventStruct. R_permutation(E) preserves No-dup-deliver(E)

By: Unfolds [`R_permutation`;`preserved_by`] 0 THEN Reduce 0 THEN Unfold `swap_adjacent` -1 THEN Reduce -1 THEN ExRepD THEN HypSubst -1 0 THEN ThinVar `y'

Generated subgoal:

1 1. E: EventStruct
2. x: |E| List
3. No-dup-deliver(E)(x)
4. i: (||x||-1)
5. True
No-dup-deliver(E)(swap(x;i;i+1))

About:

(3steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc