proposition: Lemma model_reach_pos p s c d : (forall t e, sizef t < sizep p -> t^- \in val e -> ~ eval t e) -> [p]s^+ \in val c -> reach p c d -> s^+ \in val d.
proof: Proof. Proof using cnf_S. elim: p s c d => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp|t|p IHp] s c d /= Ht. - rewrite /= /Mtrans /restrict /= /rtrans => A /andP[] /subP B _. apply: B. by rewrite RE. - move/model_of_dc => /= /andP[A B] []. + apply: IH0 => // t e H. apply: Ht. by ssrlia. + apply: IH1 => // t e H. apply: Ht. by ssrlia. - move/model_of_dc => /= A [e E1 E2]. (apply: IH1 E2; last apply: IH0 E1 => //) => t e' ?; apply Ht; by ssrlia. - move => /= A B. elim: B A => {c d} [c|c e d A _ IH B]; first by case/model_of_dc/andP. apply: IH. case/model_of_dc/andP : B => _ ?. apply: IHp A => //. move => t {e} - e A. apply: Ht. by ssrlia. - case/model_of_dc/orP; last by move => ? [->]. move => A [->] B. exfalso. apply: Ht A B. by ssrlia. - move => A. case: p {IHp Ht} A (model_of_cnf A) => //= a. rewrite /= /Mtrans /restrict /= /rtrans => A _ /andP[_] /subP B. apply: B. by rewrite RcE. Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CPDL(PDL_def)