Nuprl - Pf maction

PrintForm Definitions action sets Sections AutomataTheory Doc

1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. L1: Alph*
5. L2: Alph*
6. L: Alph*
7. (S:L1s) = (S:L2s)
8. u: Alph
9. v: Alph*
10. (S:v @ L1s) = (S:v @ L2s)

(S:(u.v) @ L1s) = (S:(u.v) @ L2s)

By: RecCaseSplit `maction`

Generated subgoals:

1 11. ((u.v) @ L1) = nil
s = (S:u.(v @ L2)s)

2 11. ((u.v) @ L1) = nil
S.act(u,(S:v @ L1s)) = (S:u.(v @ L2)s)

About:

1	11. `((u.v) @ L1) = nil` `s = (S:u.(v @ L2)s)`
2	11. `((u.v) @ L1) = nil` `S.act(u,(S:v @ L1s)) = (S:u.(v @ L2)s)`