Nuprl Definition : SM-gen-tr

SM-gen-tr(l;btrs;bp;n;m) ==
Y
(

SM-gen-tr,m.
if (

bag-null(fst((btrs m))))

(n =

m)
    then lifting-loc-2(snd((btrs m))) l (fst((btrs m))) bp
    else SM-gen-tr (m + 1)
    fi )
  m

Proof not projected

Definitions occuring in Statement : lifting-loc-2: lifting-loc-2(f), eq_int: (i =

j), bor: p

q, bnot:

b, ifthenelse: if b then t else f fi , pi1: fst(t), pi2: snd(t), ycomb: Y, apply: f a, lambda:

x.A[x], add: n + m, natural_number: $n, bag-null: bag-null(bs)
FDL editor aliases : SM-gen-tr

SM-gen-tr(l;btrs;bp;n;m) == Y (\mlambda{}SM-gen-tr,m. if (\mneg{}\msubb{}bag-null(fst((btrs m)))) \mvee{}\msubb{}(n =\msubz{} m) then lifting-loc-2(snd((btrs m))) l (fst((btrs m))) bp else SM-gen-tr (m + 1) fi ) m Date html generated: 2011_10_20-PM-03_34_26 Last ObjectModification: 2011_08_16-PM-11_51_17 Home Index