proposition: Lemma di_di' : forall t : nat, di t di_init cx_init al_init mem_init = di' t di_init cx_init al_init mem_init DC_a DC_d.
proof: Proof. 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 |- *. simple induction t. auto. intros. rewrite di_t. rewrite ad2_t. rewrite H. replace (cx n di_init cx_init al_init mem_init) with (cx' n di_init cx_init al_init mem_init DC_a DC_d). unfold cx', compo' in |- *. unfold cx3 in |- *. unfold cx_2_1, compo_2_1 in |- *. unfold di1, cx1, al1, mem1, ad1, da1 in |- *. trivial. rewrite cx_cx'. trivial. Qed.
imports: Fill_spec Fill_impl