proposition: Fact Σfull_mon_rec_sound φ : fol_sem M' φ (Σfull_mon_rec A) <-> fol_sem M φ A.
proof: Proof. Proof using M HwA. revert φ HwA; induction A as [ | r v | b B HB C HC | q B HB ]; intros φ HA. + simpl; tauto. + simpl in v; unfold Σfull_mon_rec. revert HA; vec split v with t; vec nil v; clear v; simpl vec_head; simpl syms; intros HA. specialize (HA _ (or_introl eq_refl)); simpl in HA |- *. replace (fo_term_sem M φ t) with (fo_term_sem M φ (fot_word_var (fot_word t) (fot_var t))). * simpl; apply fol_equiv_ext; do 2 f_equal. generalize (fot_word t) (fot_var t); clear t HA; intros w. induction w as [ | s w IHw ]; simpl; auto; intros i. rewrite g_snoc; simpl; do 2 f_equal; auto. * f_equal; symmetry; apply fot_word_var_eq. + simpl; apply fol_bin_sem_ext. * apply HB; intros ? ?; apply HA, in_app_iff; auto. * apply HC; intros ? ?; apply HA, 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)