GenAutomata
Sections
NuprlLIB
Doc
Def
WellFnd{i}(A;x,y.R(x;y)) ==
P:(A
Prop). (
j:A. (
k:A. R(k;j)
P(k))
P(j))
{
n:A. P(n)}
is mentioned
In prior sections:
well
fnd
int
1
int
2
GenAutomata
Sections
NuprlLIB
Doc
P:(A
Prop). (j:A. (k:A. R(k;j) 
P(k)) P(j)) {n:A. P(n)}