Library hydras.Ackermann.codeNatToTerm

From hydras.Ackermann Require Import primRec cPair code folProp folProof
                      Languages.
From Coq Require Import Arith.
From hydras.Ackermann Require LNN LNT.

Definition natToTermLNN := LNN.natToTerm.

Definition natToTermLNT := LNT.natToTerm.

Fixpoint codeNatToTerm (n: nat) : nat :=
  match n with
    0 ⇒ cPair 4 0
  | S p ⇒ cPair 3 (S (cPair (codeNatToTerm p) 0))
  end.

#[global] Instance LcodeLNN : Lcode LNN codeLNTFunction codeLNNRelation.

#[global] Instance LcodeLNT : Lcode LNT codeLNTFunction codeLNTRelation.

Lemma codeNatToTermCorrectLNN n :
 codeNatToTerm n = codeTerm (natToTermLNN n).

Lemma codeNatToTermCorrectLNT n :
 codeNatToTerm n = codeTerm (natToTermLNT n).

#[export] Instance codeNatToTermIsPR : isPR 1 codeNatToTerm.