proposition: Lemma build_store_correct: extends initial_store build_store /\ forall n a, n<build_store%s -> a < max_label -> StateLabelMap.In (n,a) build_store%d.
proof: Proof. rewrite build_store_spec. destruct (@steps_correct (power size) initial_store initiaux 0) as [H H']. simpl. pose proof (power_positive size). change 2%positive with (state_of_nat 1). num_lia. apply invariant_initial_store. simpl. auto with map. split. apply H. intros n a Hn Ha. destruct (fun H => H' (fun _ _ => False) H n a Hn Ha); try tauto. intros m b Hm _. simpl in Hm. right. right. change 2%positive with (state_of_nat 1) in Hm. num_lia. 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(Numbers) ATBR(Utils_WF)