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. u: St
6. v: St*
7. mem_f(St;s;(+f)(v)) mem_f(St;s;v) (s':St. mem_f(St;s';v) & f(s') = s)

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

By: Analyze 0 THEN Analyze -1

Generated subgoals:

1 8. u = s
u = s mem_f(St;s;v) (s':St. u = s' mem_f(St;s';v) & f(s') = s)

2 8. f(u) = s mem_f(St;s;(+f)(v))
u = s mem_f(St;s;v) (s':St. u = s' mem_f(St;s';v) & f(s') = s)

About:

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