proposition: Theorem addchains : forall (gamma : strategy) (n : nat) (M : Set) (MO : monoid M) (a : M), {b : M | b = power M MO a n}.
proof: Proof. intros gamma n M MO a; elim (zerop n); intro H; [ exists (u M MO) | exists (config_X M (Exec M MO match power_algo gamma log2_impl n H with | addchain_spec_intro gc => match gc with | gencode_intro co _ => co end end (config M a (emptystack M)))) ]. rewrite H; auto with arith. elim (power_algo gamma log2_impl n H); intro g; elim g; intros co s. inversion_clear s. rewrite H0; simpl in |- *; auto with arith. Qed.
imports: Constants generation monoid machine strategies spec log2_spec log2_implementation Compare_dec while imperative develop dicho_strat binary_strat trivial standard monofun matrix ZArith