proposition: Lemma LNN2LNT_subFormula (T : System) (f : fol.Formula LNN) (v : nat) (s : fol.Term LNN): SysPrf T (iffH (LNN2LNT_formula (substF f v s)) (substF (LNN2LNT_formula f) v (LNN2LNT_term s))).
proof: Proof. apply sysExtend with (Empty_set Formula). - intros x H; destruct H. - generalize f v s; clear T f v s; intro f. elim f using Formula_depth_ind2; intros. + simpl; rewrite (subFormulaEqual LNT). repeat rewrite LNN2LNT_subTerm; apply iffRefl. + induction r. rewrite subFormulaRelation; simpl. destruct (consTerms _ _ t) as [(a,b) p]. simpl in p; rewrite <- p. destruct (consTerms _ _ b) as [(a0,b0) p0]. simpl in p0; rewrite <- p0. rewrite translateLT1. apply iffSym; eapply iffTrans. * apply (subSubAllFormula LNT). * rewrite <- (nilTerms _ b0). replace (substTs (Tcons a (Tcons a0 (Tnil))) v s) with (Tcons (substT a v s) (Tcons (substT a0 v s) (Tnil))). rewrite translateLT1. rewrite (subAllFormula_ext LNT LTFormula (fun H : nat => nat_rec (fun _ : nat => fol.Term LNT) (LNN2LNT_term (substT a v s)) (fun (H0 : nat) (_ : fol.Term LNT) => nat_rec (fun _ : nat => fol.Term LNT) (LNN2LNT_term (substT a0 v s)) (fun (H1 : nat) (_ : fol.Term LNT) => var H1) H0) H) (fun n : nat => substT (nat_rec (fun _ : nat => fol.Term LNT) (LNN2LNT_term a) (fun (H0 : nat) (_ : fol.Term LNT) => nat_rec (fun _ : nat => fol.Term LNT) (LNN2LNT_term a0) (fun (H1 : nat) (_ : fol.Term LNT) => var H1) H0) n) v (LNN2LNT_term s))). -- apply iffRefl. -- intros m H; destruct m as [| n]. ++ simpl; apply LNN2LNT_subTerm. ++ destruct n as [| n]. ** simpl in |- *. apply LNN2LNT_subTerm. ** simpl in H. decompose sum H. discriminate H0. discriminate H1. -- reflexivity. + rewrite subFormulaImp; simpl. rewrite (subFormulaImp LNT). apply (reduceImp LNT). apply H. apply H0. + rewrite subFormulaNot. simpl; rewrite (subFormulaNot LNT). apply (reduceNot LNT). apply H. + simpl; decompose record (subFormulaForall2 LNN a v v0 s) /r. intros x H1 H0 H2 H4; rewrite H4; clear H4. decompose record (subFormulaForall2 LNT (LNN2LNT_formula a) v v0 (LNN2LNT_term s)) /r. intros x0 H4 H3 H5 H7; rewrite H7; clear H7. destruct (eq_nat_dec v v0) as [e | ]. * simpl; apply iffRefl. * simpl; apply iffTrans with (forallH x0 (substF (LNN2LNT_formula (substF (substF a v (var x)) v0 s)) x (var x0))). apply (rebindForall LNT). intros H6. assert (H7: In x0 (freeVarF (LNN2LNT_formula (substF (substF a v (var x)) v0 s)))) by (eapply List.in_remove; apply H6). assert (H8: In x0 (freeVarF (substF (substF a v (var x)) v0 s))) by (apply LNN2LNT_freeVarF1; assumption). induction (freeVarSubFormula3 _ _ _ _ _ H8). assert (H10: In x0 (freeVarF (substF a v (var x)))) by (eapply in_remove; apply H9). induction (freeVarSubFormula3 _ _ _ _ _ H10). elim H5. eapply in_in_remove. { eapply in_remove_neq, H11. } { apply LNN2LNT_freeVarF2. eapply in_remove. apply H11. } elim (in_remove_neq _ _ _ _ _ H6). destruct H11 as [H11| H11]. -- auto. -- contradiction. -- elim H4. rewrite LNN2LNT_freeVarT. assumption. -- apply (reduceForall LNT). apply (notInFreeVarSys LNT). apply iffTrans with (substF (substF (substF (LNN2LNT_formula a) v (var x)) v0 (LNN2LNT_term s)) x (var x0)). apply (reduceSub LNT). apply (notInFreeVarSys LNT). eapply iffTrans. apply H. eapply eqDepth. symmetry in |- *; rewrite subFormulaDepth; symmetry in |- *. reflexivity. apply depthForall. apply (reduceSub LNT). apply (notInFreeVarSys LNT). eapply iffTrans. apply H. apply depthForall. simpl in |- *. apply iffRefl. eapply iffTrans. apply (subFormulaExch LNT). auto. rewrite LNN2LNT_freeVarT. auto. simpl in |- *. tauto. apply (reduceSub LNT). apply (notInFreeVarSys LNT). apply (subFormulaTrans LNT). unfold not in |- *; intros; elim H2. apply in_in_remove. { eapply in_remove_neq, H6. } { apply LNN2LNT_freeVarF1. eapply in_remove. apply H6. } Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)