Nuprl Lemma : hdf-transformation-test1

hdf-buffer((λn,m. {n m}) hdf-base(m.{m});{0}) fix((λR,z. (inl a.let x ←─ in <x, {x}>)))) 0


Proof




Definitions occuring in Statement :  hdf-buffer: hdf-buffer(X;bs) hdf-compose1: X hdf-base: hdf-base(m.F[m]) callbyvalueall: callbyvalueall apply: a fix: fix(F) lambda: λx.A[x] pair: <a, b> inl: inl x add: m natural_number: $n sqequal: t single-bag: {x}
Lemmas :  false_wf le_wf subtract_wf
hdf-buffer((\mlambda{}n,m.  \{n  +  m\})  o  hdf-base(m.\{m\});\{0\})  \msim{}  fix((\mlambda{}R,z.  (inl  (\mlambda{}a.let  x  \mleftarrow{}{}  a  +  z  in  <R  x,  \{x\}>\000C))))  0



Date html generated: 2015_07_17-AM-08_17_26
Last ObjectModification: 2015_01_27-AM-11_51_31

Home Index