proposition: Lemma freeVarCodeSysPrf : forall v : nat, In v (freeVarF codeSysPrf) -> v <= 1.
proof: Proof. intros v H; unfold codeSysPrf in H. set (nv := newVar (2 :: 1 :: 0 :: v0 :: nil)) in *. repeat match goal with | H1:(?X1 = ?X2),H2:(?X1 <> ?X2) |- _ => elim H2; apply H1 | H1:(?X1 = ?X2),H2:(?X2 <> ?X1) |- _ => elim H2; symmetry in |- *; apply H1 | H:(In ?X3 (freeVarF (existH ?X1 ?X2))) |- _ => assert (In X3 (List.remove eq_nat_dec X1 (freeVarF X2))); [ apply H | clear H ] | H:(In ?X3 (freeVarF (forallH ?X1 ?X2))) |- _ => assert (In X3 (List.remove eq_nat_dec X1 (freeVarF X2))); [ apply H | clear H ] | H:(In ?X3 (List.remove eq_nat_dec ?X1 (freeVarF ?X2))) |- _ => assert (In X3 (freeVarF X2)); [ eapply in_remove; apply H | assert (X3 <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In ?X3 (freeVarF (andH ?X1 ?X2))) |- _ => assert (In X3 (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In ?X3 (freeVarF (orH ?X1 ?X2))) |- _ => assert (In X3 (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In ?X3 (freeVarF (impH ?X1 ?X2))) |- _ => assert (In X3 (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In ?X3 (freeVarF (notH LNN ?X1))) |- _ => assert (In X3 (freeVarF X1)); [ apply H | clear H ] | H:(In _ (_ ++ _)) |- _ => induction (in_app_or _ _ _ H); clear H | H:(In _ (freeVarF (substF ?X1 ?X2 ?X3))) |- _ => induction (freeVarSubFormula3 _ _ _ _ _ H); clear H | H:(In _ (freeVarF (LT ?X1 ?X2))) |- _ => rewrite freeVarLT in H | H:(In _ (freeVarT (natToTerm _))) |- _ => elim (closedNatToTerm _ _ H) | H:(In _ (freeVarT Zero)) |- _ => elim H | H:(In _ (freeVarT (Succ _))) |- _ => rewrite freeVarSucc in H | H:(In _ (@freeVarT LNN (var _))) |- _ => simpl in H; decompose sum H; clear H end. - assert (H0: Representable NN 2 (checkPrf L cL codeArityF codeArityR) (primRecFormula 2 (proj1_sig (checkPrfIsPR L cL codeArityF codeArityR codeArityFIsPR codeArityRIsPR)))) by apply primRecRepresentable. induction H0 as (H0, H4). clear H4. induction (Compat815.le_lt_or_eq _ _ (H0 _ H)). + apply le_S_n. apply H4. + elim H2; assumption. - rewrite <- H; auto. - assert (H0: Representable NN 2 codeIn (primRecFormula 2 (proj1_sig codeInIsPR))) by apply primRecRepresentable. induction H0 as (H0, H6). induction (Compat815.le_lt_or_eq _ _ (H0 _ H)). + apply le_S_n, H7. + elim H5; assumption. - elim H3. now apply freeVarfU. Qed.
imports: Coq(Ensembles) Coq(List) hydras.Ackermann(checkPrf) hydras.Ackermann(code) hydras.Ackermann(Languages) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folLogic3) hydras.Ackermann(folReplace) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(primRec) Coq(Arith Lia) hydras.Ackermann(PA) hydras.Ackermann(NNtheory) hydras.Ackermann(codeList) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(cPair) hydras.Ackermann(wellFormed) hydras.Ackermann(prLogic) hydras(Compat815)