proposition: Lemma ReplaceTermsTermSub : forall (n : nat) (ts : fol.Terms L n) (v w s2 : nat), ReplaceTermsTerm (codeTerms (substTs ts v (var w))) s2 = ReplaceTermsTerm (codeTerms ts) s2.
proof: Proof. intros n ts; unfold ReplaceTermTerm, ReplaceTermsTerm, ReplaceTermTermsTerm. 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 ?; now apply (evalStrongRecHelp2 1). } simpl in H; induction ts as [| n t ts Hrects]; simpl in |- *. - reflexivity. - intros v w s2; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; repeat rewrite computeEvalStrongRecHelp; unfold compose2; unfold evalComposeFunc, evalOneParamList, evalList; simpl in |- *; repeat rewrite cPairProjections1. unfold A at 3 1; repeat rewrite cPairProjections2; repeat rewrite H. + replace (codeTerms (Tcons (substT t v (var w)) (substTs ts v (var w)))) with (S (cPair (codeTerm (substT t v (var w))) (codeTerms (substTs ts v (var w))))); [ idtac | reflexivity ]. replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections2. replace (car (evalStrongRec 1 A (car (cPair (codeTerm t) (codeTerms ts))) s2)) with (car (evalStrongRec 1 A (car (cPair (codeTerm (substT t v (var w))) (codeTerms (substTs ts v (var w))))) s2)). * replace (cdr (evalStrongRec 1 A (codeTerms ts) s2)) with (cdr (evalStrongRec 1 A (codeTerms (substTs ts v (var w))) s2)). -- reflexivity. -- apply (Hrects v w s2). * repeat rewrite cPairProjections1. apply (ReplaceTermTermSub t v w s2). + replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections2. apply Nat.lt_succ_r, cPairLe2. + replace (codeTerms (Tcons t ts)) with (S (cPair (codeTerm t) (codeTerms ts))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections1; apply Nat.lt_succ_r, cPairLe1. + replace (codeTerms (Tcons (substT t v (var w)) (substTs ts v (var w)))) with (S (cPair (codeTerm (substT t v (var w))) (codeTerms (substTs ts v (var w))))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections2; apply Nat.lt_succ_r, cPairLe2. + replace (codeTerms (Tcons (substT t v (var w)) (substTs ts v (var w)))) with (S (cPair (codeTerm (substT t v (var w))) (codeTerms (substTs ts v (var w))))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections1; apply Nat.lt_succ_r, cPairLe1. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)