PrintForm Definitions action sets Sections AutomataTheory Doc

At: n0n1 irregular 1 1 1 1 1 1 1 1 1
1. S: ActionSet()
2. s: S.car
3. q: S.car
4. n:
5. f: S.carn
6. g: nS.car
7. InvFuns(S.car; n; f; g)
8. k:. (S:n0n1(k)s) = q
9. i: (n+1)
10. j: (n+1)
11. i < j
12. f((S:([1]i)s)) = f((S:([1]j)s))
13. g(f((S:([1]i)s))) = g(f((S:([1]j)s)))

L:*. (S:Ls) = q & (k:. L = n0n1(k))
By: RWH add_composeC 13
Generated subgoal:

113. (g o f)((S:([1]i)s)) = (g o f)((S:([1]j)s))
L:*. (S:Ls) = q & (k:. L = n0n1(k))

About:
existslistintandequalallfunction
natural_numberaddless_thanapplyconsnil