proposition: Lemma dio_repr_at_cst x i a : dio_repr_at (fun ν => ν x = i) a 6 5.
proof: Proof. exists ( (a+5,dee_add (a+0) (a+1)) ::(a+2,dee_add (a+0) (a+3)) ::(a+2,dee_add (a+1) (a+4)) ::(a+3,dee_par x) ::(a+4,dee_nat i) ::nil) (a+5); simpl; auto; try lia. + intros j c. repeat (intros [ <- | H ]; [ simpl; try lia | revert H ]); try tauto. + intros v. destruct (complete_lemma (v x) i) as (p & q & H). exists (g0 a p q (p+v x) (v x) i (p+q) 0 0); repeat constructor; simpl; rew g0; auto. + intros v; split. * intros H. exists (g0 a 0 0 (v x) (v x) i 0 0 0); repeat constructor; simpl; rew g0; auto. * intros (phi & H); revert H. repeat rewrite Forall_cons_inv; simpl; lia. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)