proposition: Lemma subAllCloseFrom1 : forall (n m : nat) (map : nat -> fol.Term L) (f : fol.Formula L) (T : fol.System L), (forall v : nat, v < n -> forall w : nat, In w (freeVarT (map (m + v))) -> w < m) -> folProof.SysPrf L T (closeFrom m n f) -> folProof.SysPrf L T (subAllFormula f (fun x : nat => match le_lt_dec m x with | left _ => match le_lt_dec (m + n) x with | left _ => var x | right _ => map x end | right _ => var x end)).
proof: Proof. intro n; induction n as [| n Hrecn]; simpl. - intros m map f T H H0; replace (subAllFormula f (fun x : nat => match le_lt_dec m x with | left _ => match le_lt_dec (m + 0) x with | left _ => var x | right _ => map x end | right _ => var x end)) with (subAllFormula f (fun x : nat => var x)). + apply (impE L) with f. * apply (iffE2 L); apply subAllFormulaId. * apply H0. + apply subAllFormula_ext. intros m0 H1; rewrite <- plus_n_O. destruct (le_lt_dec m m0); reflexivity. - intros m map f T H H0; apply (impE L) with (substF (subAllFormula f (fun x : nat => match le_lt_dec m x with | left _ => match le_lt_dec (m + n) x with | left _ => var x | right _ => map x end | right _ => var x end)) (m + n) (map (m + n))). + replace (subAllFormula f (fun x : nat => match le_lt_dec m x with | left _ => match le_lt_dec (m + S n) x with | left _ => var x | right _ => map x end | right _ => var x end)) with (subAllFormula f (fun x : nat => substT match le_lt_dec m x with | left _ => match le_lt_dec (m + n) x with | left _ => var x | right _ => map x end | right _ => var x end (m + n) (map (m + n)))). * apply (iffE1 L); apply subSubAllFormula with (m := fun x : nat => match le_lt_dec m x with | left _ => match le_lt_dec (m + n) x with | left _ => var x | right _ => map x end | right _ => var x end). * apply subAllFormula_ext. intros m0 H1; induction (le_lt_dec m m0) as [a | ?]. -- rewrite <- Compat815.plus_Snm_nSm. induction (le_lt_dec (S m + n) m0) as [a0 | ?]. ++ simpl in a0; induction (le_lt_dec (m + n) m0). ** apply (subTermVar2 L). intros H2; rewrite H2 in a0; lia. ** lia. ++ induction (le_lt_dec (m + n) m0) as [a0 | ?]. ** replace (m + n) with m0. apply (subTermVar1 L). simpl in b. rewrite Nat.lt_eq_cases in a0. destruct a0. --- lia. --- auto. ** apply (subTermNil L). intros H2; assert (H3: m + (m0 - m) = m0) by (rewrite Nat.add_comm; apply Nat.sub_add, a). assert (H4: m + n < m). { apply H with (m0 - m). apply Nat.add_lt_mono_l with m. rewrite H3. rewrite Nat.add_succ_r . apply b. rewrite H3. apply H2. } lia. -- apply (subTermVar2 L). intro H2; rewrite <- H2 in b; elim (Compat815.lt_not_le _ _ b). apply Nat.le_add_r. + apply (forallE L). apply (impE L) with (forallH (m + n) (closeFrom m n f)). * apply sysExtend with (Empty_set (fol.Formula L)). -- intros x H1; induction H1. -- apply (impI L), (forallI L). ++ intros [x [H1 H2]]; induction H2 as [x H2| x H2]; [ induction H2 | induction H2 ]. now elim (in_remove_neq _ _ _ _ _ H1). ++ apply Hrecn. ** intros v H1; eapply H; apply Nat.lt_lt_succ_r, H1. ** eapply (forallSimp L). apply Axm; right; constructor. * apply H0. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)