Nuprl - Pf switch_inv

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

E:TaggedEventStruct. safetyR(E) preserves switch_inv(E)

By: Unfolds [`preserved_by`;`R_safety`] 0 THEN Reduce 0 THEN Inst Thm* l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i < ||l1|| l1[i] = l2[i]) [|E|;y;x] THEN SimpHyp -1 THEN ExRepD THEN MoveToHyp 0 -4

Generated subgoal:

1 1. E: TaggedEventStruct
2. x: |E| List
3. y: |E| List
4. y x
5. ||y||||x||
6. i:. i < ||y|| y[i] = x[i]
7. switch_inv(E)(x)
switch_inv(E)(y)

About:

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