Nuprl Definition : equal-upto-finite-nat-seq
equal-upto-finite-nat-seq(n;f;g) == primrec(n;tt;λi,b. (b ∧b (f i =z g i)))
Definitions occuring in Statement :
band: p ∧b q,
primrec: primrec(n;b;c),
eq_int: (i =z j),
btrue: tt,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
btrue: tt,
lambda: λx.A[x],
band: p ∧b q,
eq_int: (i =z j),
apply: f a
FDL editor aliases :
equal-upto-finite-nat-seq
Latex:
equal-upto-finite-nat-seq(n;f;g) == primrec(n;tt;\mlambda{}i,b. (b \mwedge{}\msubb{} (f i =\msubz{} g i)))
Date html generated:
2016_05_14-PM-09_55_05
Last ObjectModification:
2016_01_15-AM-10_54_48
Theory : continuity
Home
Index