Library hydras.Ackermann.PAconsistent

From Coq Require Import Arith.
From hydras.Ackermann Require Import folProof folProp PA model.

Definition natModel : Model LNT :=
  model LNT nat
    (fun f : Functions LNT ⇒
     match f return (naryFunc nat (arityF LNT f)) with
     | Languages.Plus_ ⇒ fun x y : nat ⇒ y + x
     | Languages.Times_ ⇒ fun x y : nat ⇒ y × x
     | Languages.Succ_ ⇒ S
     | Languages.Zero_ ⇒ 0
     end)
    (fun r : Relations LNT ⇒ match r with end).

Theorem PAconsistent : Consistent LNT PA.