Nuprl Definition : param-W-rel
param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];par;w) ==
λn,ss,s. if (0) < (n) then (↑isl(snd(snd((ss (n - 1)))))) ∧ StepRel(ss (n - 1);s) else StepAgree(s;par;w)
Definitions occuring in Statement :
pcw-steprel: StepRel(s1;s2),
pcw-step-agree: StepAgree(s;p1;w),
assert: ↑b,
isl: isl(x),
pi2: snd(t),
and: P ∧ Q,
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
less: if (a) < (b) then c else d,
and: P ∧ Q,
assert: ↑b,
isl: isl(x),
pi2: snd(t),
pcw-steprel: StepRel(s1;s2),
apply: f a,
subtract: n - m,
natural_number: $n,
pcw-step-agree: StepAgree(s;p1;w)
FDL editor aliases :
param-W-rel
Latex:
param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];par;w) ==
\mlambda{}n,ss,s. if (0) < (n)
then (\muparrow{}isl(snd(snd((ss (n - 1)))))) \mwedge{} StepRel(ss (n - 1);s)
else StepAgree(s;par;w)
Date html generated:
2016_05_14-AM-06_13_50
Last ObjectModification:
2015_09_22-PM-05_47_12
Theory : co-recursion
Home
Index