proposition: Lemma subFormulaMinimize : forall (A B : Formula) (v x z : nat) (s : Term), ~ In x (freeVarT s) -> ~ In v (freeVarT s) -> x <> z -> v <> z -> SysPrf NN (iffH (substF (minimize A B v x) z s) (minimize (substF A z s) (substF B z s) v x)).
proof: Proof. intros A B v x z s H H0 H1 H2. unfold minimize in |- *. rewrite (subFormulaAnd LNN). rewrite (subFormulaForall LNN). destruct (eq_nat_dec x z) as [e | e]; try congruence. destruct (In_dec eq_nat_dec x (freeVarT s)) as [e0 | e0]; try tauto. rewrite (subFormulaImp LNN). unfold LT at 1 in |- *. rewrite (subFormulaRelation LNN). simpl in |- *. destruct (eq_nat_dec z x); try congruence. destruct (eq_nat_dec z v); try congruence. rewrite (subFormulaNot LNN). repeat first [ apply iffRefl | apply (reduceAnd LNN) | apply (reduceImp LNN) | apply (reduceNot LNN) | apply (reduceForall LNN); [ apply closedNN |] ]. apply (subFormulaExch LNN). - congruence. - simpl in |- *. intro H3. tauto. - auto. 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)