proposition: Lemma stepP (A : clause * annot) : A \in U -> reflect (gen A) (A \in fset.lfp U step).
proof: Proof. pose lfpE := fset.lfpE mono_step bounded_step. move => A_in_U. apply: (iffP idP) => H. - move: A H {A_in_U}. apply: fset.lfp_ind => /= A D IH. change (clause * annot)%type in A. change {fset clause * annot} in D. rewrite inE => /andP [_]. case/or3P. + case/hasP => s _. case/hasP => C _. case/hasP => E _. case/andP => [/eqP ->]. destruct s as [[|p|s t|s|s t|s t][|]] => //=; try solve [ move/IH => ?; auto | case/andP => /IH P1 /IH P2; auto ]. move => H. by rewrite (fset1U H). + case: A => C. case => [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] //=; try case/orP. * case/andP => /IH ? /IH; auto. * move => inH. by rewrite (fset1U inH). * case/andP => /IH ? /IH; auto. * move => inH. by rewrite (fset1U inH). * move/IH. exact: gen_aAXR. * case/hasP => s _. case/hasP => t _. case/hasP => C' _. case/andP => [/eqP -> /IH]. auto. * case/hasP => s _. case/hasP => t _. case/hasP => C' _. case/andP => [/eqP -> /IH]. auto. + case: A => C E /= /IH. exact: gen_jmp. - elim: H A_in_U => {A}. + move => C E inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. exact: plainP inU. + move => p C E inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply: plainP inU => /=. by rewrite !inE. + move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply: plainP (inU) => /=. by rewrite IHs ?IHt //; eauto. + move => s t C E _ IH inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply: plainP (inU) => /=. by eauto. + move => s C E _ IH inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply: plainP (inU) => /=. by eauto. + move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply: plainP (inU) => /=. rewrite IHs ?IHt //; by eauto. + move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply: plainP (inU) => /=. rewrite IHs ?IHt //; by eauto. + move => s t C _ IH inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. move/genU_foc : (inU). case/fsetXP => ?. rewrite AsAU => /andP [/sfc_F /and3P [? Hs Ht] _]. rewrite -!posE in Hs Ht. leftb. apply/hasP; exists s => //. apply/hasP; exists t => //. apply/hasP; exists C => //. rewrite eqxx /=. by eauto. + move => s t H C _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. rewrite IHs ?IHt //. exact: genU_AUhr. exact: genU_AUhl inU. + move => s t H C inU. by rewrite lfpE inE inU (_ : step_annot _ _ ) //= fset1U1. + move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply/plainP: (inU) => /=. rewrite IHs ?IHt //; by auto using genU_ARpl,genU_ARpr. + move => s t C E _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_plain _ _ ) //. apply/plainP: (inU) => /=. rewrite IHs ?IHt //; by eauto using genU_ARnl,genU_ARnr. + move => s t C _ IH inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. rightb. move/genU_foc': (inU). case/fsetXP => ?. rewrite AsAR => /andP [/sfc_F /and3P [? Hs Ht] _]. rewrite -!negE in Hs Ht. apply/hasP; exists s => //. apply/hasP; exists t => //. apply/hasP; exists C => //. rewrite eqxx IH //. exact: genU_foc'. + move => s t H C _ IHs _ IHt inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. rewrite IHs ?IHt //. exact: genU_ARhr. exact: genU_ARhl inU. + move => s t H C inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. by rewrite !inE. + move => s t H C _ IH inU. rewrite lfpE inE inU (_ : step_annot _ _ ) //=. rewrite IH //. exact: genU_aAXR. + move => C E _ IH inU. rewrite lfpE inE inU (_ : step_jmp _ _) //=. auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)