Step * of Lemma sqequal-induction-test1

hdf-buffer((λn,m. {n m}) hdf-base(m.{m});{0}) fix((λR,z. (inl a.let x ←─ in <x, {x}>)))) 0
BY
(RW (SqequalProcTrans4C []) 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