proposition: Lemma checkPrfEQnIsPR (n: nat): isPR 2 (fun p recs : nat => charFunction 2 Nat.eqb (cdr (cdr p)) 0 * charFunction 2 Nat.eqb n (car p)).
proof: Proof. unfold checkPrfEQ1; apply filter10IsPR with (g := fun p : nat => charFunction 2 Nat.eqb (cdr (cdr p)) 0 * charFunction 2 Nat.eqb n (car p)). apply compose1_2IsPR with (f := fun p : nat => charFunction 2 Nat.eqb (cdr (cdr p)) 0) (f' := fun p : nat => charFunction 2 Nat.eqb n (car p)). - apply compose1_2IsPR with (f := fun p : nat => cdr (cdr p)) (f' := fun p : nat => 0). + apply compose1_1IsPR; apply cPairPi2IsPR. + apply const1_NIsPR. + apply eqIsPR. - apply compose1_2IsPR with (f := fun p : nat => n). + apply const1_NIsPR. + apply cPairPi1IsPR. + apply eqIsPR. - apply multIsPR. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)