Nuprl Definition : vdf
vdf(A;B;a,b.C[a; b];n) ==
if n <z 1
then {L:(a:A × b:B × C[a; b]) List| ||L|| = 0 ∈ ℤ} ⟶ B ⟶ A
else f:vdf(A;B;a,b.C[a; b];n - 1) ⋂ {L:(a:A × b:B × C[a; b]) List| (||L|| ≤ n) ∧ vdf-eq(A;f;L)} ⟶ B ⟶ A
fi
Definitions occuring in Statement :
vdf-eq: vdf-eq(A;f;L),
length: ||as||,
list: T List,
dep-isect: x:A ⋂ B[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
le: A ≤ B,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
product: x:A × B[x],
subtract: n - m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
equal: s = t ∈ T,
int: ℤ,
dep-isect: x:A ⋂ B[x],
subtract: n - m,
natural_number: $n,
set: {x:A| B[x]} ,
list: T List,
product: x:A × B[x],
and: P ∧ Q,
le: A ≤ B,
length: ||as||,
vdf-eq: vdf-eq(A;f;L),
function: x:A ⟶ B[x]
FDL editor aliases :
vdf
Latex:
vdf(A;B;a,b.C[a; b];n) ==
if n <z 1
then \{L:(a:A \mtimes{} b:B \mtimes{} C[a; b]) List| ||L|| = 0\} {}\mrightarrow{} B {}\mrightarrow{} A
else f:vdf(A;B;a,b.C[a; b];n - 1) \mcap{} \{L:(a:A \mtimes{} b:B \mtimes{} C[a; b]) List| (||L|| \mleq{} n) \mwedge{} vdf-eq(A;f;L)\}
{}\mrightarrow{} B
{}\mrightarrow{} A
fi
Date html generated:
2020_05_19-PM-09_39_58
Last ObjectModification:
2020_03_05-AM-11_07_22
Theory : co-recursion-2
Home
Index