Step
*
of Lemma
bfs-predicate_wf
∀[K:RngSig]. ∀[S:Type]. ∀[P:(|K| × S) ⟶ ℙ]. ∀[b:basic-formal-sum(K;S)]. (bfs-predicate(K;S;p.P[p];b) ∈ ℙ)
BY
{ (Unfold `basic-formal-sum` 0 THEN ProveWfLemma) }
Latex:
Latex:
\mforall{}[K:RngSig]. \mforall{}[S:Type]. \mforall{}[P:(|K| \mtimes{} S) {}\mrightarrow{} \mBbbP{}]. \mforall{}[b:basic-formal-sum(K;S)].
(bfs-predicate(K;S;p.P[p];b) \mmember{} \mBbbP{})
By
Latex:
(Unfold `basic-formal-sum` 0 THEN ProveWfLemma)
Home
Index