Nuprl Definition : kripke2b-seq

kripke2b-seq(a;x;F) ==  λb.if eq-finite-seqs(a;b;x) then min-inc-seq(b;fst((F b));(a x) + 1) else 0 fi 


Definitions occuring in Statement :  eq-finite-seqs: eq-finite-seqs(a;b;x),  min-inc-seq: min-inc-seq(a;n;k),  ifthenelse: if b then t else f fi ,  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  apply: f a,  add: n + m,  pi1: fst(t),  min-inc-seq: min-inc-seq(a;n;k),  eq-finite-seqs: eq-finite-seqs(a;b;x),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x]
FDL editor aliases :  kripke2b-seq
Latex:
kripke2b-seq(a;x;F)  ==
    \mlambda{}b.if  eq-finite-seqs(a;b;x)  then  min-inc-seq(b;fst((F  b));(a  x)  +  1)  else  0  fi 


Date html generated: 2017_04_20-AM-07_37_18
Last ObjectModification: 2017_04_19-PM-03_33_08

Theory : continuity


Home Index