proposition: Fact dio_repr_at_bin o R1 a1 n1 p1 R2 a2 n2 p2 n : dio_repr_at R1 a1 n1 p1 -> dio_repr_at R2 a2 n2 p2 -> a1+n1 <= a2 -> n = 1+a2+n2-a1 -> dio_repr_at (fun ν => df_op_sem o (R1 ν) (R2 ν)) a1 n (1+p1+p2).
proof: Proof. intros [ l1 r1 F0 F1 F2 F3 F4 ] [ l2 r2 G0 G1 G2 G3 G4 ] H12 ?; subst n. exists ((a2+n2,dee_comp (dio_op_swap o) r1 r2)::l1++l2) (a2+n2). + simpl; rewrite app_length, F0, G0; lia. + replace (a1+(1+a2+n2-a1)) with (1+a2+n2) by lia. intros x c [ Hc | Hc ]. * subst; simpl; lia. * intros H1; apply in_app_or in Hc; destruct Hc as [ Hc | Hc ]. - specialize (F1 _ _ Hc H1); lia. - specialize (G1 _ _ Hc H1); lia. + lia. + intros f. destruct (F3 f) as (g1 & H1). destruct (G3 f) as (g2 & H2). destruct (@valuation_one_union (a2+n2) (de_op_sem (dio_op_swap o) (g1 r1) (g2 r2)) (a1,a1+n1) g1 (a2,a2+n2) g2) as (g & Hg1 & Hg2 & Hg3); auto using not_interval_union. { red; simpl; intros; lia. } exists g; constructor; [ | apply Forall_app; split ]. * simpl; rewrite Hg1, (Hg2 r1), (Hg3 r2); auto. * apply Forall_impl with (2 := H1). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg2, F1 with c; auto. * apply Forall_impl with (2 := H2). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg3, G1 with c; auto. + intros f. destruct o; simpl; rewrite F4, G4; split. * intros [ (g1 & H1 & H2) | (g2 & H1 & H2) ]. - destruct (G3 f) as (g2 & H3). destruct (@valuation_one_union (a2+n2) 0 (a1,a1+n1) g1 (a2,a2+n2) g2) as (g & Hg1 & Hg2 & Hg3); auto using not_interval_union. { red; simpl; intros; lia. } exists g; split; auto. constructor; simpl; [ | apply Forall_app; split ]. ++ rewrite Hg1, Hg2, H2; auto. ++ apply Forall_impl with (2 := H1). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg2, F1 with c; auto. ++ apply Forall_impl with (2 := H3). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg3, G1 with c; auto. - destruct (F3 f) as (g1 & H3). destruct (@valuation_one_union (a2+n2) 0 (a1,a1+n1) g1 (a2,a2+n2) g2) as (g & Hg1 & Hg2 & Hg3); auto using not_interval_union. { red; simpl; intros; lia. } exists g; split; auto. constructor; simpl; [ | apply Forall_app; split ]. ++ rewrite Hg1, (Hg3 r2), H2, Nat.mul_comm; auto. ++ apply Forall_impl with (2 := H3). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg2, F1 with c; auto. ++ apply Forall_impl with (2 := H1). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg3, G1 with c; auto. * intros (g & Hg1 & Hg2). inversion Hg1 as [ | ? ? Hg3 Hg4 ]. apply Forall_app in Hg4; destruct Hg4 as (Hg4 & Hg5). simpl in Hg3; rewrite Hg2 in Hg3. symmetry in Hg3; apply Nat.eq_mul_0 in Hg3. destruct Hg3 as [ Hg3 | Hg3 ]; [ left | right ]; exists g; auto. * intros ((g1 & H1 & H2) & (g2 & H3 & H4)). destruct (@valuation_one_union (a2+n2) 0 (a1,a1+n1) g1 (a2,a2+n2) g2) as (g & Hg1 & Hg2 & Hg3); auto using not_interval_union. { red; simpl; intros; lia. } exists g; split; auto; constructor; simpl. ++ rewrite Hg1, Hg2, Hg3; auto; lia. ++ apply Forall_app; split. ** apply Forall_impl with (2 := H1). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg2, F1 with c; auto. ** apply Forall_impl with (2 := H3). intros c Hc; apply dc_eval_ext; auto. intros x Hx; apply Hg3, G1 with c; auto. * intros (g & Hg1 & Hg2). inversion Hg1 as [ | ? ? Hg3 Hg4 ]. apply Forall_app in Hg4; destruct Hg4 as (Hg4 & Hg5). simpl in Hg3; split; exists g; split; auto; lia. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)