Nuprl Definition : eq-finite-seqs
eq-finite-seqs(a;b;x) == primrec(x;tt;λi,r. (r ∧b (a i =z b 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 :
apply: f a,
eq_int: (i =z j),
band: p ∧b q,
lambda: λx.A[x],
btrue: tt,
primrec: primrec(n;b;c)
FDL editor aliases :
eq-finite-seqs
Latex:
eq-finite-seqs(a;b;x) == primrec(x;tt;\mlambda{}i,r. (r \mwedge{}\msubb{} (a i =\msubz{} b i)))
Date html generated:
2017_04_20-AM-07_37_02
Last ObjectModification:
2017_04_18-AM-10_39_25
Theory : continuity
Home
Index