Step
*
of Lemma
dl-forces-trivial
No Annotations
∀K:dl_KS. ∀phi:Prop. ∀s:worlds(K). dl_forces(K;tt;phi
⇒ phi;s)
BY
{ (Auto THEN ((Unfold `dl_forces` 0 THEN Reduce 0) THEN Auto) THEN Try (Fold `dl_forces` 0) THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}K:dl\_KS. \mforall{}phi:Prop. \mforall{}s:worlds(K). dl\_forces(K;tt;phi {}\mRightarrow{} phi;s)
By
Latex:
(Auto THEN ((Unfold `dl\_forces` 0 THEN Reduce 0) THEN Auto) THEN Try (Fold `dl\_forces` 0) THEN Auto)
Home
Index