Nuprl - Pf switch_inv_rel

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

1. E: TaggedEventStruct
2. tr: |E| List
3. ls: ||tr||
4. switch_inv(E)(tr)
5. i: ||tr||
6. j: ||tr||
7. i (switchR(tr)^*) ls
8. j (switchR(tr)^*) ls

tag(E)(tr[i]) = tag(E)(tr[j])

By: Inst Thm* R,R2:(TTProp). Trans(T)(R2(_1,_2)) (x,y:T. (x R y) (x R2 y)) (x,y:T. (x (R^*) y) (x R2 y) x = y) [||tr||;switchR(tr);i,j. tag(E)(tr[i]) = tag(E)(tr[j])] THEN Try ((Unfolds [`trans`;`refl`] 0) THEN (ReduceSOAps 0)) THEN All ReduceSOAps THEN All Reduce

Generated subgoals:

1 9. x: ||tr||
10. y: ||tr||
11. x switchR(tr) y
tag(E)(tr[x]) = tag(E)(tr[y])

2 9. x,y:||tr||. (x (switchR(tr)^*) y) tag(E)(tr[x]) = tag(E)(tr[y]) x = y
tag(E)(tr[i]) = tag(E)(tr[j])

About:

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

1	9. `x:` `\|\|tr\|\|` 10. `y:` `\|\|tr\|\|` 11. `x switchR(tr) y` `tag(E)(tr[x]) = tag(E)(tr[y])`
2	9. `x,y:\|\|tr\|\|. (x (switchR(tr)^*) y) tag(E)(tr[x]) = tag(E)(tr[y]) x = y` `tag(E)(tr[i]) = tag(E)(tr[j])`