proposition: Lemma eval_change_initial : eval (change_initial A i') == eval (change_initial A j').
proof: Proof. apply mx_to_scal_compat. pose (y := box _ _ (fun np rp => xif (state_of_nat np =T= state_of_nat rp) 1 0): KMX (nat_of_num size) (nat_of_num size)). pose (m := MAUT.delta (to_MAUT (change_initial A j'))). pose (v := MAUT.final (to_MAUT (change_initial A j'))). apply (equiv_filter (y := y) (m := m) (v := v)). simpl MAUT.initial. fold_regex. setoid_rewrite (mx_point_one_left (n:=1) (m:=size) (p:=size)). mx_intros a b Ha Hb. simpl. fold_regex. apply xif_compat; auto. rewrite 2 id_num. apply <- bool_prop_iff. rewrite 2 T_true. destruct tarjan_correct as [[ _ _ _ H] _]. rewrite H. tauto. num_lia. num_lia. mx_intros i k Hi Hk. simpl; fold_regex. apply sum_leq; intros j _ Hj. xif_destruct; [semiring_normalize|semiring_reflexivity]. unfold labelling. setoid_rewrite sum_distr_left. rewrite sum_inversion. apply sum_incr; intros a Ha. simpl; fold_regex. fold_leq. xif_destruct; unfold xif at 1; trivial with algebra. leq_sum (delta a i). pose proof (bounded_delta Hbounds a i). num_lia. bool_simpl. num_prop. rewrite H0. rewrite (simulation H); trivial. unfold xif. semiring_reflexivity. num_lia. num_lia. mx_intros i j Hi Hj. clear - Hi Hbounds i' Hi' Hj' _H. simpl; fold_regex. apply leq_antisym. apply sum_leq. intros n Hn Hn'. xif_destruct; [semiring_normalize|semiring_reflexivity]. apply T_finaux in H. unfold statesetelt_of_nat, statemapelt_of_nat in *. rewrite H. reflexivity. xif_destruct; trivial with algebra. leq_sum i. rewrite T_refl, H. xif_simpl. semiring_reflexivity. mx_intros i j Hi Hj. simpl; fold_regex. nat_analyse; auto with algebra. rewrite T_refl. xif_simpl. trivial with algebra. mx_intros i j Hi Hj. simpl; fold_regex. apply sum_leq. intros k Hk Hk'. xif_destruct; [semiring_normalize|semiring_reflexivity]. xif_destruct; [semiring_normalize|semiring_reflexivity]. rewrite T_true in *. rewrite H0 in H. rewrite <- T_true in H. rewrite H. reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_StateSetSets) ATBR(Utils_WF) Coq(Relations) Coq(List)