Step
*
of Lemma
interface-fifo_wf
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:E(X) ─→ E]. (interface-fifo(es;X;f) ∈ ℙ)
BY
{ (Unfold `interface-fifo` 0 THEN Auto) }
Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(Top)]. \mforall{}[f:E(X) {}\mrightarrow{} E]. (interface-fifo(es;X;f) \mmember{} \mBbbP{})
By
(Unfold `interface-fifo` 0 THEN Auto)
Home
Index