proposition: Remark minimize1 : forall (A B : Formula) (v x : nat), v <> x -> ~ In x (freeVarF B) -> forall a : nat, SysPrf NN (substF A v (n2t a)) -> SysPrf NN (substF B v (n2t a)) -> (forall b : nat, b < a -> SysPrf NN (notH (substF A v (n2t b)))) -> (forall b : nat, b < a -> SysPrf NN (notH (substF B v (n2t b)))) -> SysPrf NN (iffH (minimize A B v x) (equal (var v) (n2t a))).
proof: Proof. intros A B v x H H0 a H1 H2 H3 H4. apply iffI. unfold minimize in |- *. apply impI. apply impE with (substF (impH (LT (var x) (var v)) (notH (substF B v (var x)))) x (n2t a)). - rewrite (subFormulaImp LNN). rewrite (subFormulaNot LNN). apply impTrans with (impH (LT (n2t a) (var v)) (notH (substF B v (n2t a)))). + apply iffE1. apply (reduceImp LNN). * unfold LT at 2 in |- *. rewrite (subFormulaRelation LNN). simpl in |- *. destruct (eq_nat_dec x x) as [e | e]; try lia. destruct (eq_nat_dec x v). -- elim H. auto. -- apply iffRefl. * apply (reduceNot LNN). apply (subFormulaTrans LNN). intro H5. elim H0. eapply in_remove. exact H5. + apply impTrans with (notH (LT (n2t a) (var v))). * apply impI. apply impE with (notH (notH (substF B v (n2t a)))). apply cp2. -- apply Axm; right; constructor. -- apply nnI. do 2 apply sysWeaken. exact H2. * apply impE with (notH (LT (var v) (n2t a))). apply orE with (LT (var v) (n2t a)) (orH (equal (var v) (n2t a)) (LT (n2t a) (var v))). -- apply sysWeaken. apply nn9. -- repeat apply impI. apply contradiction with (LT (var v) (n2t a)). ++ apply Axm; left; left; right; constructor. ++ apply Axm; left; right; constructor. -- apply impI. apply orSys; repeat apply impI. ++ apply Axm; left; left; right; constructor. ++ apply contradiction with (LT (n2t a) (var v)). ** apply Axm; left; left; right; constructor. ** apply Axm; right; constructor. -- apply impE with (notH (notH A)). apply cp2. ++ apply sysWeaken. apply boundedLT. intros n H5. rewrite (subFormulaNot LNN). auto. ++ apply nnI. eapply andE1. apply Axm; right; constructor. - apply forallE. eapply andE2. apply Axm; right; constructor. - apply impI. unfold minimize in |- *. rewrite <- (subFormulaId LNN (andH A (forallH x (impH (LT (var x) (var v)) (notH (substF B v (var x)))))) v). apply impE with (substF (andH A (forallH x (impH (LT (var x) (var v)) (notH (substF B v (var x)))))) v (n2t a)). + apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. + apply sysWeaken. rewrite (subFormulaAnd LNN). apply andI. * auto. * rewrite (subFormulaForall LNN). destruct (eq_nat_dec x v) as [e | e]; try congruence. destruct (In_dec eq_nat_dec x (freeVarT (n2t a))) as [e0 | e0]. -- elim (closedNatToTerm _ _ e0). -- apply forallI. apply closedNN. rewrite (subFormulaImp LNN). unfold LT in |- *. rewrite (subFormulaRelation LNN). simpl in |- *. destruct (eq_nat_dec v v) as [e1 | e1]; try congruence. ++ induction (eq_nat_dec v x) as [e2 | e2]; try congruence. apply impI. apply forallE. apply forallI. intro H5. destruct H5 as (x0, H5); destruct H5 as (H5, H6). destruct H6 as [x0 H6 | x0 H6]. ** elim closedNN with v. exists x0; auto. ** destruct H6. destruct H5 as [H5 | H5]; try congruence. fold (freeVarT (n2t a)) in H5. simpl in H5. rewrite app_nil_r in H5. elim (closedNatToTerm _ _ H5). ** apply impE with (LT (var x) (n2t a)). --- apply sysWeaken. apply boundedLT. intros n H5. rewrite (subFormulaNot LNN). apply impE with (notH (substF B v (n2t n))). +++ apply cp2. apply iffE1. apply (subFormulaTrans LNN). intro H6. elim H0. eapply in_remove. exact H6. +++ apply H4; auto. --- apply Axm; right; constructor. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)