fact: Definition codeSubFormula (f v s : nat) : nat := let C := cPair 0 (pow3 f + (v + (s + f))) in car (boundedSearch (fun p x : nat => ltBool 0 (checkSubFormulaTrace (cPair (car p) x))) (cPair (cTriple v s f) (S (boundComputation f (cTriple C C (ReplaceFormulaTerm f C)) (ReplaceFormulaTerm f C))))).
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)