proposition: Lemma dio_repr_at_op o x y z a : dio_repr_at (fun ν => ν x = de_op_sem o (ν y) (ν z)) a 8 7.
proof: Proof. exists ( (a+7,dee_add (a+0) (a+1)) ::(a+6,dee_add (a+0) (a+2)) ::(a+6,dee_add (a+1) (a+5)) ::(a+5,dee_comp o (a+3) (a+4)) ::(a+2,dee_par x) ::(a+3,dee_par y) ::(a+4,dee_par z) ::nil) (a+7); simpl; auto; try lia. + intros j c. repeat (intros [ <- | H ]; [ simpl; try lia | revert H ]); try tauto. + intros v. destruct (complete_lemma (v x) (de_op_sem o (v y) (v z))) as (p & q & H). exists (g0 a p q (v x) (v y) (v z) (de_op_sem o (v y) (v z)) (p+v x) (p+q)); repeat constructor; simpl; rew g0; auto. + intros v; split. * intros H. exists (g0 a 0 0 (v x) (v y) (v z) (v x) (v x) 0); repeat constructor; simpl; rew g0; auto. * intros (phi & H); revert H. repeat rewrite Forall_cons_inv; simpl. intros ((E1 & E2 & E3 & E4 & E5 & E6 & E7 & _) & E0). rewrite <- E6, <- E7, <- E4; lia. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)