fact: Fixpoint codePrf (Z : Formulas) (f : Formula) (prf : Prf Z f) {struct prf} : nat := match prf with | AXM A => cPair 0 (codeFormula A) | MP Axm1 Axm2 A B rec1 rec2 => cPair 1 (cPair (cPair (cPair 1 (cPair (codeFormula A) (codeFormula B))) (codePrf _ _ rec1)) (cPair (codeFormula A) (codePrf _ _ rec2))) | GEN Axm A v _ rec => cPair 2 (cPair v (cPair (codeFormula A) (codePrf _ _ rec))) | IMP1 A B => cPair 3 (cPair (codeFormula A) (codeFormula B)) | IMP2 A B C => cPair 4 (cPair (codeFormula A) (cPair (codeFormula B) (codeFormula C))) | CP A B => cPair 5 (cPair (codeFormula A) (codeFormula B)) | FA1 A v t => cPair 6 (cPair (codeFormula A) (cPair v (codeTerm t))) | FA2 A v _ => cPair 7 (cPair (codeFormula A) v) | FA3 A B v => cPair 8 (cPair (codeFormula A) (cPair (codeFormula B) v)) | EQ1 => cPair 9 0 | EQ2 => cPair 10 0 | EQ3 => cPair 11 0 | EQ4 r => cPair 12 (codeR cl r) | EQ5 f => cPair 13 (codeF cl f) end.
imports: Coq(Arith) hydras.Ackermann(fol folProof cPair)