Library hydras.Ackermann.prLogic
prLogic.v
Original script by Russel O'Connor
Although this module doesn't depend on FOL, the following lemmas are JUST helpers to prove that the encoding of basic FOL connectives are PR
From
hydras.Ackermann
Require
Import
primRec
code
cPair
.
From
Coq
Require
Import
Arith
.
Lemma
codeForallIsPR
:
isPR
2 (
fun
a
b
:
nat
⇒
cPair
3 (
cPair
a
b
)).
#[
export
]
Instance
codeNotIsPR
:
isPR
1
codeNot
.
#[
export
]
Instance
codeImpIsPR
:
isPR
2
codeImp
.