proposition: Lemma mem_mem' : forall t : nat, mem t di_init cx_init al_init mem_init = mem' t di_init cx_init al_init mem_init DC_a DC_d.
proof: Proof. unfold mem', compo' in |- *. unfold mem3 in |- *. unfold mem_2_1, compo_2_1 in |- *. unfold di1, cx1, al1, mem1, ad1, da1 in |- *. simple induction t. auto. intros. rewrite mem2_t. rewrite mem_t. rewrite H. replace (al n di_init cx_init al_init mem_init) with al_init. replace (da2 n di_init cx_init al_init mem_init di_init al_init) with al_init. rewrite (di_di' n). unfold di' in |- *. unfold compo' in |- *. unfold di3 in |- *. unfold ad_2_1, compo_2_1 in |- *. unfold di1, cx1, al1, mem1, ad1, da1 in |- *. rewrite (cx_cx' n). unfold cx', compo', cx3 in |- *. unfold cx_2_1, compo_2_1 in |- *. unfold di1, cx1, al1, mem1, ad1, da1 in |- *. trivial. rewrite da2_constant. trivial. rewrite al_constant. trivial. Qed.
imports: Fill_spec Fill_impl