proposition: Lemma subAllCloseFrom : forall (n : nat) (m : nat -> fol.Term L) (f : fol.Formula L) (T : fol.System L), folProof.SysPrf L T (closeFrom 0 n f) -> folProof.SysPrf L T (subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => m x end)).
proof: Proof. intros n m f T H; assert (H0: exists r : nat, (forall v : nat, v < n -> newVar (freeVarT (m v)) <= r)). { clear H T f; induction n as [| n Hrecn]. - exists 0; intros v H; lia. - destruct Hrecn as [x H]; exists (max (newVar (freeVarT (m n))) x). + intros v H0; assert (H1: v <= n) by lia. induction (Compat815.le_lt_or_eq _ _ H1). * apply Nat.le_trans with x. -- apply H; auto. -- apply Nat.le_max_r. * rewrite H2; apply Nat.le_max_l. } destruct H0 as (x, H0). set (r := max (max n (newVar (freeVarF f))) x). set (f' := subAllFormula f (fun x : nat => match le_lt_dec n x with | left _ => var x | right _ => var (r + x) end)). set (m' := fun x : nat => m (x - r)). apply (impE L) with (subAllFormula f' (fun x : nat => match le_lt_dec r x with | left _ => match le_lt_dec (r + n) x with | left _ => var x | right _ => m' x end | right _ => var x end)). - replace (subAllFormula f (fun x0 : nat => match le_lt_dec n x0 with | left _ => var x0 | right _ => m x0 end)) with (subAllFormula f (fun x : nat => subAllTerm match le_lt_dec n x with | left _ => var x | right _ => var (r + x) end (fun x0 : nat => match le_lt_dec r x0 with | left _ => match le_lt_dec (r + n) x0 with | left _ => var x0 | right _ => m' x0 end | right _ => var x0 end))). + apply (iffE1 L). unfold f'; apply subAllSubAllFormula with (m1 := fun x0 : nat => match le_lt_dec n x0 with | left _ => var x0 | right _ => var (r + x0) end) (m2 := fun x0 : nat => match le_lt_dec r x0 with | left _ => match le_lt_dec (r + n) x0 with | left _ => var x0 | right _ => m' x0 end | right _ => var x0 end). + unfold m'; apply subAllFormula_ext; intros m0 H1. induction (le_lt_dec n m0) as [a | ?]. * simpl; induction (le_lt_dec r m0) as [a0 | ?]. -- rewrite Nat.le_ngt in a0; destruct a0. apply Nat.lt_le_trans with (newVar (freeVarF f)). ++ now apply newVar2. ++ unfold r; eapply Nat.le_trans. ** apply Nat.le_max_r. ** apply Nat.le_max_l. -- reflexivity. * simpl; induction (le_lt_dec r (r + m0)) as [a | ?]. -- induction (le_lt_dec (r + n) (r + m0)). ++ lia. ++ f_equal; lia. -- lia. - apply subAllCloseFrom1. + intros v H1 w H2; apply Nat.lt_le_trans with (newVar (freeVarT (m v))). * apply newVar2. unfold m' in H2; now replace (r + v - r) with v in H2 by lia. * apply Nat.le_trans with x. -- now apply H0. -- unfold r; apply Nat.le_max_r. + unfold f'; clear f'; apply liftCloseFrom. * intros v H1; apply Nat.lt_le_trans with (newVar (freeVarF f)). -- now apply newVar2. -- unfold r; eapply Nat.le_trans. ++ apply Nat.le_max_r. ++ apply Nat.le_max_l. * unfold r; eapply Nat.le_trans. -- apply Nat.le_max_l. -- apply Nat.le_max_l. * apply H. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)