Nuprl Definition : lifting-gen-list-rev

lifting-gen-list-rev(n;bags) ==
  fix((λlifting-gen-list-rev,m,g. if (n =z m) then {g} else ⋃x∈bags m.lifting-gen-list-rev (m + 1) (g x) fi ))


Definitions occuring in Statement :  bag-combine: ⋃x∈bs.f[x],  single-bag: {x},  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  single-bag: {x},  bag-combine: ⋃x∈bs.f[x],  add: n + m,  natural_number: $n,  apply: f a
FDL editor aliases :  lifting-gen-list-rev
Latex:
lifting-gen-list-rev(n;bags)  ==
    fix((\mlambda{}lifting-gen-list-rev,m,g.  if  (n  =\msubz{}  m)
                                                                  then  \{g\}
                                                                  else  \mcup{}x\mmember{}bags  m.lifting-gen-list-rev  (m  +  1)  (g  x)
                                                                  fi  ))


Date html generated: 2016_05_15-PM-02_59_04
Last ObjectModification: 2015_09_23-AM-07_40_43

Theory : bags


Home Index