Nuprl - Pf trace_inv_as

(12steps) PrintForm Definitions Lemmas mb state machine Sections GenAutomata Doc

1. M: sm{i:l}()
2. P: M.state(M.action List)Prop
3. (M |= s,t.P(s,t) while True)
4. (M |= initially s,t.P(s,t))

(M |= always s,t.P(s,t))

By: Unfold `while` -2 THEN Unfold `tla` -2 THEN BackThru Thm* M:sm{i:l}(), I:(M.state(M.action List)Prop). (x:M.state. M.init(x) I(x,nil)) (s0,x:M.state, act:M.action, x':M.state, l:M.action List. M.init(s0) trace_reachable(M;s0;l;x) I(x,l) M.trans(x,act,x') I(x',l @ [act])) (M |= always s,t.I(s,t))

Generated subgoals:

1 3. s,x':M.state, t:M.action List, a:M.action. (M -t- > s) M.trans(s,a,x') P(s,t) True True P(x',t @ [a])
4. (M |= initially s,t.P(s,t))
5. x: M.state
6. M.init(x)
P(x,nil)

2 3. s,x':M.state, t:M.action List, a:M.action. (M -t- > s) M.trans(s,a,x') P(s,t) True True P(x',t @ [a])
4. (M |= initially s,t.P(s,t))
5. s0: M.state
6. x: M.state
7. act: M.action
8. x': M.state
9. l: M.action List
10. M.init(s0)
11. trace_reachable(M;s0;l;x)
12. P(x,l)
13. M.trans(x,act,x')
P(x',l @ [act])

About:

(12steps) PrintForm Definitions Lemmas mb state machine Sections GenAutomata Doc

1	3. `s,x':M.state, t:M.action List, a:M.action. (M -t- > s) M.trans(s,a,x') P(s,t) True True P(x',t @ [a])` 4. `(M \|= initially s,t.P(s,t))` 5. `x:` `M.state` 6. `M.init(x)` `P(x,nil)`
2	3. `s,x':M.state, t:M.action List, a:M.action. (M -t- > s) M.trans(s,a,x') P(s,t) True True P(x',t @ [a])` 4. `(M \|= initially s,t.P(s,t))` 5. `s0:` `M.state` 6. `x:` `M.state` 7. `act:` `M.action` 8. `x':` `M.state` 9. `l:` `M.action List` 10. `M.init(s0)` 11. `trace_reachable(M;s0;l;x)` 12. `P(x,l)` 13. `M.trans(x,act,x')` `P(x',l @ [act])`