fact: Definition checkPrfMP (p recs : nat) := switchPR (wellFormedFormula (car (cdr (cdr (cdr p)))) * (charFunction 2 Nat.eqb (car (car (cdr (cdr p)))) (codeImp (car (cdr (cdr (cdr p)))) (car p)) * (codeNth (p - S (caddr p)) recs * codeNth (p - S (cdddr p)) recs))) (S (codeApp (pred (codeNth (p - S (caddr p)) recs)) (pred (codeNth (p - S (cdr (cdr (cdr p)))) recs)))) 0.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)