Nuprl - Pf add_action

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

St:Type, l:St*, f:(StSt), s:St. mem_f(St;s;(+f)(l)) mem_f(St;s;l) (s':St. mem_f(St;s';l) & f(s') = s)

By: GenExRepD

Generated subgoals:

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

2 1. St: Type
2. l: St*
3. f: StSt
4. s: St
5. mem_f(St;s;l)
mem_f(St;s;(+f)(l))

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

About:

1	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)`
2	1. `St:` `Type` 2. `l:` `St*` 3. `f:` `StSt` 4. `s:` `St` 5. `mem_f(St;s;l)` `mem_f(St;s;(+f)(l))`
3	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))`