Nuprl - Pf switch_normal

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

E:TaggedEventStruct, tr:Trace(E). (switch_inv(E) No-dup-send(E))(tr) (tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr'))

By: Unfolds [`prop_and`;`str_trace`] 0 THEN Reduce 0 THEN Inst Thm* L:T List, P:(TTProp). (x,y:T. Dec(P(x,y))) (x,y:T. P(x,y) P(y,x)) (L':T List. (L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)]))) [|E|;tr;R_ad_normal(tr)] THEN Reduce 0 THEN Try (Complete (Auto THEN Easy))

Generated subgoals:

1 1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
x,y:|E|. R_ad_normal(tr)(x,y) R_ad_normal(tr)(y,x)

2 1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
5. L':|E| List. (tr (swap adjacent[R_ad_normal(tr)(x,y)]^*) L') & (i:(||L'||-1). R_ad_normal(tr)(L'[i],L'[(i+1)]))
tr':|E| List. switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')

About:

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

1	1. `E:` `TaggedEventStruct` 2. `tr:` `\|E\| List` 3. `switch_inv(E)(tr)` 4. `No-dup-send(E)(tr)` `x,y:\|E\|. R_ad_normal(tr)(x,y) R_ad_normal(tr)(y,x)`
2	1. `E:` `TaggedEventStruct` 2. `tr:` `\|E\| List` 3. `switch_inv(E)(tr)` 4. `No-dup-send(E)(tr)` 5. `L':\|E\| List. (tr (swap adjacent[R_ad_normal(tr)(x,y)]^*) L') & (i:(\|\|L'\|\|-1). R_ad_normal(tr)(L'[i],L'[(i+1)]))` `tr':\|E\| List. switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')`