Library Goedel.fixPoint

From hydras.Ackermann Require Import primRec.
From hydras.Ackermann Require Import cPair.
From Coq Require Import Arith Lia.
From hydras.Ackermann Require Import code.
From hydras.Ackermann Require Import codeSubFormula.
From hydras.Ackermann Require Import folProp.
From hydras.Ackermann Require Import folProof.
From hydras.Ackermann Require Import Languages.
From hydras.Ackermann Require Import subAll.
From hydras.Ackermann Require Import subProp.
From hydras.Ackermann Require Import folLogic3.
From hydras.Ackermann Require Import folReplace.
From hydras.Ackermann Require Import LNN.
From hydras.Ackermann Require Import codeNatToTerm.
From Goedel Require Import PRrepresentable.
From hydras.Ackermann Require Import ListExt.
From Coq Require Import List.
From hydras.Ackermann Require Import NN.
From hydras.Ackermann Require Import expressible.
From hydras Require Import Compat815.
Import FolNotations.
Import NNnotations.

Definition subStar (a v n : nat) : nat := codeSubFormula a v (codeNatToTerm n).

#[export] Instance subStarIsPR : isPR 3 subStar.

Section LNN_FixPoint.

Let codeFormula := codeFormula (cl:=LcodeLNN).

Lemma FixPointLNN :
 ∀ (A : Formula) (v : nat),
 {B : Formula |
   SysPrf NN
     (B ↔ substF A v (natToTermLNN (codeFormula B)))%fol ∧
   (∀ x : nat,
    In x (freeVarF B) ↔
    In x (List.remove eq_nat_dec v (freeVarF A)))}.

End LNN_FixPoint.

From hydras.Ackermann Require Import PA.
From hydras.Ackermann Require Import NN2PA.

Section LNT_FixPoint.

Let codeFormula := codeFormula (cl:=LcodeLNT).

Lemma FixPointLNT (A : Formula) (v : nat):
  {B : Formula |
    SysPrf PA
      (iffH B (substF A v (natToTermLNT (codeFormula B)))) ∧
      (∀ x : nat,
          In x (freeVarF B) ↔
            In x (List.remove eq_nat_dec v (freeVarF A)))}.

End LNT_FixPoint.