PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
n0n1
irregular
1
1
1
1
1
1
1
1
1
1
1
1
1
1
1
2
1
1.
S:
ActionSet(
)
2.
s:
S.car
3.
q:
S.car
4.
n:
5.
f:
S.car
n
6.
g:
n
S.car
7.
g o f = Id
8.
f o g = Id
9.
k:
. (S:n0n1(k)
s) = q
10.
i:
(n+1)
11.
j:
(n+1)
12.
i < j
13.
f((S:([1]
i)
s)) = f((S:([1]
j)
s))
14.
(S:([1]
i)
s) = (S:([1]
j)
s)
15.
k:
(([0]
j) @ ([1]
i)) = n0n1(k)
By:
Analyze 0
Generated subgoal:
1
16.
(([0]
j) @ ([1]
i)) = n0n1(k)
False
About:
j) @ ([1]i)) = n0n1(k)
False
)
nnS.car
k:. (S:n0n1(k)
s) = q(n+1)(n+1)i)s)) = f((S:([1]j)s))i)s) = (S:([1]j)s) 
(([0]j) @ ([1]i)) = n0n1(k)j) @ ([1]i)) = n0n1(k) False
