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