---

Step * of 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
BY
{ (RW (SqequalProcTrans4C []) 0 THEN Auto) }

---

Latex:


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


By

(RW  (SqequalProcTrans4C  [])  0  THEN  Auto)

---

Home Index