proposition: Lemma clean_factorise_leq_weq l: l ≪ BOT+CKA -> forall n m (x y: expr n m), (x <==_[BOT+l] y -> clean x = 0%ast \/ clean x <==_[l] clean y) /\ (x ==_[BOT+l] y -> clean x ==_[l] clean y).
proof: Proof. intros Hl. apply expr_leq_weq_ind. constructor; [constructor; [constructor|..] |..]; simpl ob in *; discr_levels Hl ltac:(fun Hl' => apply lower_bot in Hl'; [|reflexivity]); intro_vars; destruct_tests; try solve [intuition (reflexivity || discriminate)]. intros [Hx|Hxy]. now left. intros [Hy|Hyz]. left. revert Hy. generalize (clean_leq_0 Hl Hxy). now rewrite 2clean_idem. right. etransitivity; eassumption. rewrite weq_spec. split. intros [? ?]; split; now right. intros [[Hx|Hx] [Hy|Hy]]. rewrite Hx, Hy. now split. generalize (clean_leq_0 Hl Hy). rewrite 2clean_idem. intro Hy'. now rewrite Hx, Hy'. generalize (clean_leq_0 Hl Hx). rewrite 2clean_idem. intro Hx'. now rewrite Hx', Hy. now split. rewrite cup_spec. intuition discriminate. intros; apply dotA. intros; apply dot1x. intros; apply dotx1. intros ? ? ? [Hx|Hxy] H'. tauto. generalize (clean_leq_0 Hl Hxy). rewrite clean_idem. tauto. intros ? ? ? ? [Hx|Hxy] H'. tauto. destruct H' as [Hx'|Hxy']. tauto. generalize (clean_leq_0 Hl Hxy'). rewrite clean_idem. tauto. right. apply dot_leq; tauto. right. now rewrite dotplsx. right. now rewrite dotxpls. right. apply cnvdot_. intros; apply cnv_invol. intros ? ? [Hx|Hxy]. tauto. generalize (clean_leq_0 Hl Hxy). rewrite clean_idem. tauto. right. apply cnv_leq. tauto. right. apply cnv_ext. right. apply str_refl. right. apply str_cons. right. now rewrite dot1x. right. apply str_ind_l; intuition discriminate. right. now rewrite dotx1. right. apply str_ind_r; intuition discriminate. intros _ _. apply itr_str_l. Qed.
imports: kleene syntax