proposition: Fact Σfull_mon_rec_complete φ : fol_sem M' φ (Σfull_mon_rec A) <-> fol_sem M φ A.
proof: Proof. Proof using HwA HM1' HM2'. revert φ HwA; induction A as [ | r v | b B HB C HC | q B HB ]; intros φ HwA. + simpl; tauto. + simpl in v; unfold Σfull_mon_rec. revert HwA; vec split v with t; vec nil v; clear v; simpl vec_head; simpl syms; intros HwA. specialize (HwA _ (or_introl eq_refl)); simpl in HwA |- *. replace (fo_term_sem M φ t) with (fo_term_sem M φ (fot_word_var (fot_word t) (fot_var t))). * revert HwA; generalize (fot_word t) (fot_var t); intros w i. rewrite <- (rev_length w), <- Hf. simpl; generalize (rev w) (φ i); clear w; intros w. induction w as [ | s w IHw ]; simpl; auto; intros Hw x. - rewrite HM2'; tauto. - rewrite HM1', IHw; simpl; try tauto; lia. * f_equal; symmetry; apply fot_word_var_eq. + apply fol_bin_sem_ext. * apply HB; intros ? ?; apply HwA, in_app_iff; auto. * apply HC; intros ? ?; apply HwA, in_app_iff; auto. + simpl; apply fol_quant_sem_ext; intro; apply HB; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat Sig_no_syms)