Step
*
1
1
of Lemma
radd-list_functionality
1. 0 = 0 ∈ ℤ
2. ∀i:ℕ0. (⊥ = ⊥)
⊢ bdd-diff(λn.0;λn.0)
BY
{ (RelRST THEN Auto) }
Latex:
Latex:
1.  0  =  0
2.  \mforall{}i:\mBbbN{}0.  (\mbot{}  =  \mbot{})
\mvdash{}  bdd-diff(\mlambda{}n.0;\mlambda{}n.0)
By
Latex:
(RelRST  THEN  Auto)
Home
Index