Nuprl Lemma : sqequal-induction-test1
hdf-buffer((λn,m. {n + m}) o hdf-base(m.{m});{0}) ~ fix((λR,z. (inl (λa.let x ←─ a + z in <R x, {x}>)))) 0
Proof
Definitions occuring in Statement :
hdf-buffer: hdf-buffer(X;bs),
hdf-compose1: f o X,
hdf-base: hdf-base(m.F[m]),
callbyvalueall: callbyvalueall,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
pair: <a, b>,
inl: inl x,
add: n + m,
natural_number: $n,
sqequal: s ~ 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_25
Last ObjectModification:
2015_01_27-AM-11_51_25
Home
Index