proposition: Lemma HBL1 : forall f, SysPrf T f -> SysPrf T (box f).
proof: Proof. intros x H; unfold box. apply impE with (LNN2LNT_formula (substF codeSysPf 0 (LNN.natToTerm (codeFormula x)))). replace (natToTerm (codeFormula x)) with (LNN2LNT_term (LNN.natToTerm (codeFormula x))). - apply iffE1; apply LNN2LNT_subFormula. - induction (codeFormula x) as [| n IHn]. + reflexivity. + simpl; rewrite IHn; reflexivity. - assert (H0: forall f : fol.Formula LNN, mem (fol.Formula LNN) T' f -> exists Axm : Formulas, ex (fun _ : Prf LNT Axm (LNN2LNT_formula f) => forall g : Formula, In g Axm -> mem (fol.Formula LNT) T g) /\ (forall v : nat, In v (freeVarListFormula LNT Axm) -> In v (freeVarF f))). { intros f H0; destruct H0 as [x0 H0|]. - assert (H1: SysPrf PA (LNN2LNT_formula x0)). { apply NN2PA. apply (folLogic.Axm). assumption. } destruct H1 as [x1 [x2 H1]]. exists x1; split. + exists x2; intros g H2. apply extendsPA. apply H1; assumption. + intros v H2; elim closedPA with v. destruct (In_freeVarListFormulaE _ _ _ H2) as [x3 H3]. exists x3; split. * tauto. * apply H1; tauto. - exists ((LNN2LNT_formula x0)::nil); split. + exists (AXM LNT (LNN2LNT_formula x0)); intros g H1. simpl in H1; destruct H1 as [H1 | H1]. * rewrite <- H1; apply H0. * contradiction. + intros v H1. destruct (In_freeVarListFormulaE _ _ _ H1) as [x1 H2]. simpl in H2. destruct H2 as [H2 H3]. * destruct H3. -- rewrite <- H3 in H2. apply LNN2LNT_freeVarF1. assumption. -- contradiction. } destruct (codeSysPfCorrect _ H) as [x0 [x1 H1]]. destruct (translatePrf T' T H0 (substF codeSysPf 0 (LNN.natToTerm (codeFormula x))) x0 x1 H1) as [x2 H2]. exists x2; destruct H2; assumption. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) Goedel(fixPoint) hydras.Ackermann(NN2PA) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) Goedel(rosserPA)