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
1
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:
16.
(([0]
j) @ ([1]
i)) = (([0]
k) @ ([1]
k))
17.
k = i
False
By:
ApFunToHypEquands `L' ||0:L||
16
Generated subgoal:
1
18.
||0:([0]
j) @ ([1]
i)|| = ||0:([0]
k) @ ([1]
k)||
False
About: