Nuprl - Pf add_action

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. St: Type
2. l: St*
3. f: StSt
4. s: St
5. s': St
6. f(s') = s
7. u: St
8. v: St*
9. mem_f(St;s';v) mem_f(St;s;(+f)(v))

u = s' mem_f(St;s';v) u = s f(u) = s mem_f(St;s;(+f)(v))

By: Analyze 0 THEN Analyze -1

Generated subgoals:

1 10. u = s'
u = s f(u) = s mem_f(St;s;(+f)(v))

2 10. mem_f(St;s';v)
u = s f(u) = s mem_f(St;s;(+f)(v))

About:

1	10. `u = s'` `u = s f(u) = s mem_f(St;s;(+f)(v))`
2	10. `mem_f(St;s';v)` `u = s f(u) = s mem_f(St;s;(+f)(v))`