Nuprl - Pf trace_inv_as

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

By: Unfold `trace_inv` -1 THEN Unfold `initially` 0 THEN InstHyp [nil;s;s] -3

Generated subgoal:

1 3. t:M.action List, s0,s:M.state. M.init(s0) trace_reachable(M;s0;t;s) P(s,t)
4. s: M.state
5. M.init(s)
trace_reachable(M;s;nil;s)

About: