proposition: Lemma build_store_spec: build_store = steps (power size) initial_store initiaux (state_of_nat 0).
proof: Proof. unfold build_store. pose (Heq:=powerfix_linearfix (A:=Store) (B:=stateset -> num -> Store) (R:=pointwise_relation _ (pointwise_relation _ (@eq _)))). rewrite Heq. generalize (state_of_nat 0) initiaux initial_store. generalize (power size) as n. induction n; intros s p np; simpl. reflexivity. apply fold_num_compat, step_compat. repeat intro. apply IHn. intros f g H s ? <- p np. apply fold_num_compat, step_compat. unfold pointwise_relation; simpl. apply H. 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)