PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
min
el
sound
1
1
1.
E:
2.
n:
3.
EquivRel x,y:
. x E y
E(n,MinArg(E(n) : {0..n
}))
By:
RWH (LemmaC
Thm*
f:(
), n:
. f(MinArg(f : {0..n
})) = f(n)) 0
Generated subgoal:
1
E(n,n)
About:
E(n,n)
. x E y E(n,MinArg(E(n) : {0..n
}))
f:(), n:. f(MinArg(f : {0..n})) = f(n))
0 E(n,n)
