Nuprl - Pf switch_normal

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

E:TaggedEventStruct. safetyR(E) preserves AD-normal(E)

By: Unfolds [`preserved_by`;`R_safety`] 0 THEN Reduce 0 THEN Try (Fold `trace_property` 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. AD-normal(E)(x)
AD-normal(E)(y)

About:

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