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

mem_f(St;s;l) (s':St. mem_f(St;s';l) & f(s') = s)

By: ListInd 2

Generated subgoals:

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

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

About:

1	`mem_f(St;s;(+f)(nil)) mem_f(St;s;nil) (s':St. mem_f(St;s';nil) & f(s') = s)`
2	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)` `mem_f(St;s;(+f)(u.v)) mem_f(St;s;u.v) (s':St. mem_f(St;s';u.v) & f(s') = s)`