Step * of Lemma st-ptr_wf

[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  (ptr(tab) ∈ ℕ)
BY
(Unfolds ``secret-table st-ptr`` THEN Auto) }


Latex:


Latex:
\mforall{}[T:Id  {}\mrightarrow{}  Type].  \mforall{}[tab:secret-table(T)].    (ptr(tab)  \mmember{}  \mBbbN{})


By


Latex:
(Unfolds  ``secret-table  st-ptr``  0  THEN  Auto)




Home Index