Step
*
of Lemma
bfs-equiv_wf
∀[K:RngSig]. ∀[S:Type]. ∀[a,b:basic-formal-sum(K;S)].  (bfs-equiv(K;S;a;b) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[K:RngSig].  \mforall{}[S:Type].  \mforall{}[a,b:basic-formal-sum(K;S)].    (bfs-equiv(K;S;a;b)  \mmember{}  \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index