Nuprl - Pf switch_normal

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

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)

By: All (h.(Unfold `switch_normal` h) THEN (Reduce h)) THEN ParallelOp -1 THEN Thin -3 THEN Subst (y[i] = x[i]) 0 THEN EasyHyp THEN Subst (y[(i+1)] = x[(i+1)]) 0 THEN EasyHyp

Generated subgoal:

1 7. i: (||y||-1)
8. (is-send(E)(x[i]) is-send(E)(x[(i+1)]) (x[i] =msg=(E) x[(i+1)])) & ((x@0,y:||x||. x@0 < y & is-send(E)(x[x@0]) & is-send(E)(x[y]) & x[x@0] delivered at time i+1 & x[y] delivered at time i) loc(E)(x[i]) = loc(E)(x[(i+1)]))
(is-send(E)(x[i]) is-send(E)(x[(i+1)]) (x[i] =msg=(E) x[(i+1)])) & ((x,y@0:||y||. x < y@0 & is-send(E)(y[x]) & is-send(E)(y[y@0]) & y[x] delivered at time i+1 & y[y@0] delivered at time i) loc(E)(x[i]) = loc(E)(x[(i+1)]))

About:

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