proposition: Lemma subAllSubAllFormula (T : fol.System L) (f : fol.Formula L): forall (m1 m2 : nat -> fol.Term L), folProof.SysPrf L T (iffH (subAllFormula (subAllFormula f m1) m2) (subAllFormula f (fun n : nat => subAllTerm (m1 n) m2))).
proof: Proof. revert T. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]. - intros T m1 m2; simpl; repeat rewrite subAllSubAllTerm; apply (iffRefl L). - intros T m1 m2; simpl; rewrite subAllSubAllTerms. apply (iffRefl L). - intros T m1 m2; simpl; apply (reduceImp L). + apply Hrecf1. + apply Hrecf0. - intros T m1 m2; simpl; apply (reduceNot L). apply Hrecf. - intros T m1 m2; simpl; set (nv1 := freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) m1). set (nv2 := freeVarF f ++ freeVarMap (List.remove eq_nat_dec n (freeVarF f)) (fun n0 : nat => subAllTerm (m1 n0) m2)). set (nv3 := freeVarF (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var (newVar nv1) | right _ => m1 v end)) ++ freeVarMap (List.remove eq_nat_dec (newVar nv1) (freeVarF (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var (newVar nv1) | right _ => m1 v end)))) m2). apply (iffTrans L) with (forallH (newVar nv3) (substF (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var (newVar nv2) | right _ => subAllTerm (m1 v) m2 end)) (newVar nv2) (var (newVar nv3)))). + eapply (sysExtend L) with (Empty_set (fol.Formula L)). * intros x H; contradiction H. * apply (reduceForall L). -- apply (notInFreeVarSys L). -- eapply (iffTrans L). ++ apply Hrecf. ++ set (a1 := fun v : nat => match eq_nat_dec v n with | left _ => var (newVar nv2) | right _ => subAllTerm (m1 v) m2 end). simpl; set (a2 := fun n0 : nat => subAllTerm match eq_nat_dec n0 n with | left _ => var (newVar nv1) | right _ => m1 n0 end (fun v : nat => match eq_nat_dec v (newVar nv1) with | left _ => var (newVar nv3) | right _ => m2 v end)). replace (subAllFormula f a2) with (subAllFormula f (fun x : nat => substT (a1 x) (newVar nv2) (var (newVar nv3)))). ** apply (iffSym L). apply subSubAllFormula. ** apply subAllFormula_ext. intros m H. unfold a1, a2; induction (eq_nat_dec m n). --- rewrite (subTermVar1 L). simpl; induction (eq_nat_dec (newVar nv1) (newVar nv1)) as [? | b]. +++ reflexivity. +++ now elim b. --- auto. rewrite subSubAllTerm. apply subAllTerm_ext. intros m0 H0; induction (eq_nat_dec m0 (newVar nv1)) as [a | ?]. +++ elim (newVar1 nv1). rewrite <- a. unfold nv1; apply in_or_app; right. eapply freeVarMap1. *** apply H0. *** apply in_in_remove; auto. +++ apply (subTermNil L). intro H1. elim (newVar1 nv2). unfold nv2 at 2; apply in_or_app; right. eapply freeVarMap1. *** eapply freeVarSubAllTerm2. apply H0. apply H1. *** apply in_in_remove; auto. + apply (iffSym L). apply (rebindForall L). intro H; assert (H0:In (newVar nv3) (freeVarF (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var (newVar nv2) | right _ => subAllTerm (m1 v) m2 end)))) by (eapply in_remove; apply H). decompose record (freeVarSubAllFormula1 _ _ _ H0) /r; intros x H2 H3. induction (eq_nat_dec x n). * induction H3 as [H1| H1]. -- elim (in_remove_neq _ _ _ _ _ H). ++ auto. -- contradiction. * decompose record (freeVarSubAllTerm1 _ _ _ H3) /r; intros x0 H4 H5. elim (newVar1 nv3). unfold nv3 at 2; apply in_or_app. right; eapply freeVarMap1. -- apply H5. -- apply in_in_remove. ++ intro H1; elim (newVar1 nv1). rewrite <- H1; unfold nv1; apply in_or_app; right. eapply freeVarMap1. apply H4. apply in_in_remove; auto. ++ eapply freeVarSubAllFormula2. ** apply H2. ** induction (eq_nat_dec x n) as [a | ?]. --- now elim b. --- assumption. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)