proposition: Lemma ReplaceTermTermSub : forall (t : fol.Term L) (v w s2 : nat), ReplaceTermTerm (codeTerm (substT t v (var w))) s2 = ReplaceTermTerm (codeTerm t) s2.
proof: Proof. intro t; 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)). 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 n m H; apply (evalStrongRecHelp2 1); assumption. } simpl in H; elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => forall v w s2 : nat, ReplaceTermsTerm (codeTerms (substTs ts v (var w))) s2 = ReplaceTermsTerm (codeTerms ts) s2); simpl in |- *; intros; unfold evalStrongRec in |- *; unfold evalComposeFunc, evalOneParamList, evalList in |- *; repeat rewrite computeEvalStrongRecHelp; unfold compose2 in |- *; unfold evalComposeFunc, evalOneParamList, evalList in |- *; simpl in |- *; repeat rewrite cPairProjections1. - induction (eq_nat_dec v n); (replace (codeTerm (var n)) with (cPair 0 n); [ idtac | reflexivity ]). + replace (codeTerm (var w)) with (cPair 0 w); [ idtac | reflexivity ]. unfold A at 3 1 in |- *. repeat rewrite cPairProjections1. simpl; reflexivity. + reflexivity. - replace (codeTerm (apply f (substTs t0 v (var w)))) with (cPair (S (cf f)) (codeTerms (substTs t0 v (var w)))); [ idtac | reflexivity ]. unfold A at 3 1 in |- *. repeat rewrite cPairProjections1. replace (codeTerm (apply f t0)) with (cPair (S (cf f)) (codeTerms t0)); [ idtac | reflexivity ]. repeat rewrite H. + repeat rewrite cPairProjections1. simpl; repeat rewrite cPairProjections2. replace (cdr (evalStrongRec 1 A (codeTerms (substTs t0 v (var w))) s2)) with (cdr (evalStrongRec 1 A (codeTerms t0) s2)); [reflexivity | ]. symmetry; apply (H0 v w s2). + repeat rewrite cPairProjections2. apply cPairLt2. + repeat rewrite cPairProjections2. apply cPairLt2. - reflexivity. - unfold ReplaceTermsTerm; unfold ReplaceTermsTerm in H1. unfold ReplaceTermTermsTerm; unfold ReplaceTermTermsTerm in H1. fold A in H1 |- *. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. unfold A at 3 1; repeat rewrite cPairProjections2; repeat rewrite H. + replace (codeTerms (Tcons (substT t0 v (var w)) (substTs t1 v (var w)))) with (S (cPair (codeTerm (substT t0 v (var w))) (codeTerms (substTs t1 v (var w))))); [ idtac | reflexivity ]. replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections2. replace (car (evalStrongRec 1 A (car (cPair (codeTerm t0) (codeTerms t1))) s2)) with (car (evalStrongRec 1 A (car (cPair (codeTerm (substT t0 v (var w))) (codeTerms (substTs t1 v (var w))))) s2)). * replace (cdr (evalStrongRec 1 A (codeTerms t1) s2)) with (cdr (evalStrongRec 1 A (codeTerms (substTs t1 v (var w))) s2)). -- reflexivity. -- apply (H1 v w s2). * repeat rewrite cPairProjections1. apply (H0 v w s2). + replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections2. apply Nat.lt_succ_r. apply cPairLe2. + replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections1; apply Nat.lt_succ_r. apply cPairLe1. + replace (codeTerms (Tcons (substT t0 v (var w)) (substTs t1 v (var w)))) with (S (cPair (codeTerm (substT t0 v (var w))) (codeTerms (substTs t1 v (var w))))); [ idtac | reflexivity ]. simpl; rewrite cPairProjections2; apply Nat.lt_succ_r. apply cPairLe2. + replace (codeTerms (Tcons (substT t0 v (var w)) (substTs t1 v (var w)))) with (S (cPair (codeTerm (substT t0 v (var w))) (codeTerms (substTs t1 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)