PrintForm Definitions action sets Sections AutomataTheory Doc

At: maction lemma 1 2 2 1
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)
11. ((u.v) @ L1) = nil

S.act(u,(S:v @ L2s)) = (S:u.(v @ L2)s)
By: RW (AddrC [3] (RecUnfoldC `maction`)) 0
Generated subgoal:

1 S.act(u,(S:v @ L2s)) = if null(u.(v @ L2)) s else S.act(hd((u.(v @ L2))),(S:tl((u.(v @ L2)))s)) fi

About:
equalapplyconsuniverselistnilifthenelse