Nuprl Definition : init-seg-nat-seq
init-seg-nat-seq(f;g) == let n,s = f in let m,r = g in if ble(n;m) then equal-upto-finite-nat-seq(n;s;r) else ff fi
Definitions occuring in Statement :
equal-upto-finite-nat-seq: equal-upto-finite-nat-seq(n;f;g),
ble: ble(n;m),
ifthenelse: if b then t else f fi ,
bfalse: ff,
spread: spread def
Definitions occuring in definition :
spread: spread def,
ifthenelse: if b then t else f fi ,
ble: ble(n;m),
equal-upto-finite-nat-seq: equal-upto-finite-nat-seq(n;f;g),
bfalse: ff
FDL editor aliases :
init-seg-nat-seq
Latex:
init-seg-nat-seq(f;g) ==
let n,s = f
in let m,r = g
in if ble(n;m) then equal-upto-finite-nat-seq(n;s;r) else ff fi
Date html generated:
2016_05_14-PM-09_55_18
Last ObjectModification:
2016_01_15-AM-11_03_40
Theory : continuity
Home
Index