Nuprl - Pf switch_inv_rel_closure

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

1. E: EventStruct
2. tr: |E| List
3. ls: ||tr||
4. is-send(E)(tr[ls])
5. j:||tr||. ls < j is-send(E)(tr[j])

i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)

By: Assert (n:, i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls))

Generated subgoals:

1 n:, i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls)

2 6. n:, i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls)
i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)

About:

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

1	`n:, i,j:\|\|tr\|\|. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls)`
2	6. `n:, i,j:\|\|tr\|\|. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^) ls)` `i,j:\|\|tr\|\|. ij is-send(E)(tr[j]) (i (switchR(tr)^) ls) (j (switchR(tr)^*) ls)`