fact: Definition makeTrace : fol.Formula L -> nat * fol.Term L -> nat := Formula_depth_rec2 L (fun _ : fol.Formula L => nat * fol.Term L -> nat) (fun (t t0 : fol.Term L) (p : nat * fol.Term L) => let v := fst p in let s := snd p in cTriple (cTriple v (codeTerm s) (codeFormula (equal t t0))) (codeFormula (substF (equal t t0) v s)) 0) (fun (r : Relations L) t (p : nat * fol.Term L) => let v := fst p in let s := snd p in cTriple (cTriple v (codeTerm s) (codeFormula (atomic r t))) (codeFormula (substF (atomic r t) v s)) 0) makeTraceImp makeTraceNot makeTraceForall.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)