proposition: Lemma subSubAllFormula : forall (T : fol.System L) (f : fol.Formula L) (m : nat -> fol.Term L) (v : nat) (s : fol.Term L), folProof.SysPrf L T (iffH (substF (subAllFormula f m) v s) (subAllFormula f (fun n : nat => substT (m n) v s))).
proof: Proof. intros T f. revert T. elim f using Formula_depth_ind2; simpl in |- *. - intros t t0 T m v s; rewrite (subFormulaEqual L). do 2 rewrite subSubAllTerm. apply (iffRefl L). - intros r t T m v s; rewrite (subFormulaRelation L). rewrite subSubAllTerms; apply (iffRefl L). - intros f0 H f1 H0 T m v s; rewrite (subFormulaImp L). apply (reduceImp L). + apply H. + apply H0. - intros f0 H T m v s; rewrite (subFormulaNot L). apply (reduceNot L). apply H. - intros v a H T m v0 s; set (nv1 := newVar (freeVarF a ++ freeVarMap (List.remove eq_nat_dec v (freeVarF a)) m)). set (nv2 := newVar (freeVarF a ++ freeVarMap (List.remove eq_nat_dec v (freeVarF a)) (fun n : nat => substT (m n) v0 s))). apply (sysExtend L) with (Empty_set (fol.Formula L)). + unfold Included; intros x H0; destruct H0. + decompose record (subFormulaForall2 L (subAllFormula a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var nv1 | right _ => m v1 end)) nv1 v0 s) /r; intros x H1 H0 H2 H4. rewrite H4; clear H4. induction (eq_nat_dec nv1 v0) as [a0 | ?]. * assert (H3: forall n : nat, In n (freeVarF (forallH v a)) -> substT (m n) v0 s = m n). { intros n H3; apply subTermNil. intros H4. elim (newVar1 (freeVarF a ++ freeVarMap (List.remove eq_nat_dec v (freeVarF a)) m)). fold nv1; rewrite a0. apply in_or_app; right. eapply freeVarMap1. apply H4. apply H3. } assert (H4: nv1 = nv2). { unfold nv1, nv2; rewrite (freeVarMap_ext (List.remove eq_nat_dec v (freeVarF a)) (fun n : nat => substT (m n) v0 s) m). - reflexivity. - apply H3. } rewrite H4. rewrite (subAllFormula_ext a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var nv2 | right _ => substT (m v1) v0 s end) (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var nv2 | right _ => m v1 end)). -- apply (iffRefl L). -- intros m0 H5; induction (eq_nat_dec m0 v). ++ reflexivity. ++ apply H3; simpl; apply in_in_remove; auto. * apply (iffTrans L) with (forallH x (substF (subAllFormula a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => m v1 end)) v0 s)). -- apply (reduceForall L). ++ apply (notInFreeVarSys L). ++ apply (reduceSub L). ** apply (notInFreeVarSys L). ** apply (iffTrans L) with (subAllFormula a (fun v1 : nat => substT match eq_nat_dec v1 v with | left _ => var nv1 | right _ => m v1 end nv1 (var x))). --- fold (folProof.SysPrf L); apply H with (b := a) (v := nv1) (s := var x) (m := fun v1 : nat => match eq_nat_dec v1 v with | left _ => var nv1 | right _ => m v1 end). apply depthForall. --- rewrite (subAllFormula_ext a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => m v1 end) (fun v1 : nat => substT match eq_nat_dec v1 v with | left _ => var nv1 | right _ => m v1 end nv1 (var x))). +++ apply (iffRefl L). +++ intros m0 H3. induction (eq_nat_dec m0 v). *** rewrite (subTermVar1 L); reflexivity. *** rewrite (subTermNil L). reflexivity. intro H4; elim (newVar1 (freeVarF a ++ freeVarMap (List.remove eq_nat_dec v (freeVarF a)) m)). fold nv1; apply in_or_app. right. eapply freeVarMap1. apply H4. apply in_in_remove; auto. -- apply (iffTrans L) with (forallH x (subAllFormula a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => substT (m v1) v0 s end))). ++ apply (reduceForall L). ** apply (notInFreeVarSys L). ** eapply (iffTrans L). --- apply H with (b := a) (v := v0) (s := s) (m := fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => m v1 end). apply depthForall. --- rewrite (subAllFormula_ext a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => substT (m v1) v0 s end) (fun n : nat => substT match eq_nat_dec n v with | left _ => var x | right _ => m n end v0 s)). +++ apply (iffRefl L). +++ intros m0 H3; induction (eq_nat_dec m0 v). *** rewrite subTermNil. reflexivity. simpl; tauto. *** reflexivity. ++ apply (iffTrans L) with (forallH nv2 (substF (subAllFormula a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => substT (m v1) v0 s end)) x (var nv2))). ** apply (rebindForall L). intros H3; simpl in H3. assert (H4: In nv2 (freeVarF (subAllFormula a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var x | right _ => substT (m v1) v0 s end)))) by (eapply in_remove; apply H3). decompose record (freeVarSubAllFormula1 _ _ _ H4) /r; intros x0 H6 H7. induction (eq_nat_dec x0 v) as [a0 | ?]. --- induction H7 as [H5| H5]. +++ elim (in_remove_neq _ _ _ _ _ H3); auto. +++ auto. --- elim (newVar1 (freeVarF a ++ freeVarMap (List.remove eq_nat_dec v (freeVarF a)) (fun n : nat => substT (m n) v0 s))). fold nv2; apply in_or_app. right; eapply freeVarMap1. +++ apply H7. +++ apply in_in_remove; auto. ** apply (reduceForall L). --- apply (notInFreeVarSys L). --- eapply (iffTrans L). +++ apply H. apply depthForall. +++ simpl; rewrite (subAllFormula_ext a (fun v1 : nat => match eq_nat_dec v1 v with | left _ => var nv2 | right _ => substT (m v1) v0 s end) (fun n : nat => substT match eq_nat_dec n v with | left _ => var x | right _ => substT (m n) v0 s end x (var nv2))). *** apply (iffRefl L). *** intros m0 H3; induction (eq_nat_dec m0 v). rewrite (subTermVar1 L). reflexivity. rewrite (subTermNil L (substT (m m0) v0 s)). reflexivity. intros H4; induction (freeVarSubTerm3 _ _ _ _ _ H4). elim H2. apply in_in_remove. intros H6; elim (newVar1 (freeVarF a ++ freeVarMap (List.remove eq_nat_dec v (freeVarF a)) m)). fold nv1; rewrite <- H6. apply in_or_app. right; eapply freeVarMap1. eapply in_remove. apply H5. apply in_in_remove; auto. eapply freeVarSubAllFormula2. apply H3. induction (eq_nat_dec m0 v). elim b0; auto. eapply in_remove. apply H5. auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)