Nuprl - Pf trace_inv_as

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

M:sm{i:l}(), P:(M.state(M.action List)Prop). (M |= always s,t.P(s,t)) (M |= s,t.P(s,t) while True) & (M |= initially s,t.P(s,t))

By: Auto

Generated subgoals:

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

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

3 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))

About:

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

1	1. `M:` `sm{i:l}()` 2. `P:` `M.state(M.action List)Prop` 3. `(M \|= always s,t.P(s,t))` `(M \|= s,t.P(s,t) while True)`
2	1. `M:` `sm{i:l}()` 2. `P:` `M.state(M.action List)Prop` 3. `(M \|= always s,t.P(s,t))` `(M \|= initially s,t.P(s,t))`
3	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))`