PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
7
1
1
1
1
1
1.
Alph:
Type
2.
R:
Alph*
Alph*
Prop
3.
n:
4.
L:
Alph*
5.
m:
6.
x:Alph*. R(x,x)
7.
x,y:Alph*. R(x,y)
R(y,x)
8.
x,y,z:Alph*. R(x,y) & R(y,z)
R(x,z)
9.
x,y,z:Alph*. R(x,y)
R((z @ x),z @ y)
10.
w:(
n
Alph*).
l:Alph*.
i:
n. R(l,w(i))
11.
v:(
m
Alph*).
l:Alph*. L(l)
(
i:
m. R(l,v(i)))
12.
Fin(Alph)
13.
x:
Alph*
14.
y:
Alph*
15.
l:
Alph*
16.
L(l @ x) = L(l @ y)
k:
(n
n), l:{l:(Alph*)| ||l|| = k
}.
L(l @ x) = L(l @ y)
By:
Inst
Thm*
R:(Alph*
Alph*
Prop), n:
. (
x:Alph*. R(x,x)) & (
x,y:Alph*. R(x,y)
R(y,x)) & (
x,y,z:Alph*. R(x,y) & R(y,z)
R(x,z)) & (
x,y,z:Alph*. R(x,y)
R((z @ x),z @ y)) & (
w:(
n
Alph*).
l:Alph*.
i:
n. R(l,w(i)))
(
a,b,c:Alph*.
a':Alph*. ||a'|| < n
n & R((a @ b),a' @ b) & R((a @ c),a' @ c)) [Alph;R;n]
Generated subgoals:
1
(
x:Alph*. R(x,x)) & (
x,y:Alph*. R(x,y)
R(y,x)) & (
x,y,z:Alph*. R(x,y) & R(y,z)
R(x,z)) & (
x,y,z:Alph*. R(x,y)
R((z @ x),z @ y)) & (
w:(
n
Alph*).
l:Alph*.
i:
n. R(l,w(i)))
2
17.
a,b,c:Alph*.
a':Alph*. ||a'|| < n
n & R((a @ b),a' @ b) & R((a @ c),a' @ c)
k:
(n
n), l:{l:(Alph*)| ||l|| = k
}.
L(l @ x) = L(l @ y)
About: