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. mem_f(St;s';l)
7. f(s') = s

mem_f(St;s;(+f)(l))

By: ListInd 2

Generated subgoals:

1 6. f(s') = s
mem_f(St;s';nil) mem_f(St;s;(+f)(nil))

2 6. f(s') = s
7. u: St
8. v: St*
9. mem_f(St;s';v) mem_f(St;s;(+f)(v))
mem_f(St;s';u.v) mem_f(St;s;(+f)(u.v))

About:

1	6. `f(s') = s` `mem_f(St;s';nil) mem_f(St;s;(+f)(nil))`
2	6. `f(s') = s` 7. `u:` `St` 8. `v:` `St*` 9. `mem_f(St;s';v) mem_f(St;s;(+f)(v))` `mem_f(St;s';u.v) mem_f(St;s;(+f)(u.v))`