proposition: Lemma boundSubTerms : forall (n : nat) (ts : fol.Terms L n) (v : nat) (s : fol.Term L), codeTerms (substTs ts v s) <= ReplaceTermsTerm (codeTerms ts) (fold_right Nat.max 0 (codeTerm s :: freeVarTs ts)).
proof: Proof. intros n ts. unfold ReplaceTermTerm in |- *. unfold ReplaceTermsTerm in |- *. unfold ReplaceTermTermsTerm in |- *. set (A := fun t0 recs s0 : nat => cPair (switchPR (car t0) (cPair (car t0) (cdr (codeNth (t0 - S (cdr t0)) recs))) (cPair 0 s0)) (switchPR t0 (S (cPair (car (codeNth (t0 - S (car (pred t0))) recs)) (cdr (codeNth (t0 - S (cdr (pred t0))) recs)))) 0)) in *. assert (H: forall n m : nat, m < n -> extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 A n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 A m)). { intros n0 m; apply (evalStrongRecHelp2 1); assumption. } simpl in H; induction ts as [| n t ts Hrects]; simpl in |- *. - intros v s; apply Nat.le_0_l. - intros v s; replace (codeTerms (Tcons (substT t v s) (substTs ts v s))) with (S (cPair (codeTerm (substT t v s)) (codeTerms (substTs ts v s)))); [ idtac | reflexivity ]. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; repeat rewrite computeEvalStrongRecHelp; unfold compose2; unfold evalComposeFunc, evalOneParamList, evalList; simpl in |- *; repeat rewrite cPairProjections1. unfold A at 1; repeat rewrite cPairProjections2; repeat rewrite H. + replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections1. apply le_n_S; apply cPairLe3. * eapply Nat.le_trans. -- apply boundSubTerm. -- apply (ReplaceTermTermMonotone (codeTerm t) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarT t))) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarTs (Tcons t ts))))). apply maxLemma. ++ apply le_n. ++ replace (freeVarTs (Tcons t ts)) with (freeVarT t ++ freeVarTs ts); [ idtac | reflexivity ]. apply maxLemma2. * eapply Nat.le_trans. -- apply Hrects. -- repeat rewrite cPairProjections2. apply (ReplaceTermsTermMonotone (codeTerms ts) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarTs ts))) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarTs (Tcons t ts))))). apply maxLemma. ++ apply le_n. ++ replace (freeVarTs (Tcons t ts)) with (freeVarT t ++ freeVarTs ts); [ idtac | reflexivity ]. apply maxLemma3. + replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections2. apply Nat.lt_succ_r. apply cPairLe2. + replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections1. apply Nat.lt_succ_r, cPairLe1. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)