fact: Definition checkSubFormulaTrace : nat -> nat := evalStrongRec 0 (fun trace recs : nat => let v := cTriplePi1 (cTriplePi1 trace) in let s := cTriplePi2 (cTriplePi1 trace) in let input := cTriplePi3 (cTriplePi1 trace) in let output := cTriplePi2 trace in let rest := cTriplePi3 trace in let type := cPairPi1 input in switchPR type (switchPR (pred type) (switchPR (pred (pred type)) (switchPR (pred (pred (pred type))) (charFunction 2 Nat.eqb output (cPair type (codeSubTerms (cdr input) v s))) (switchPR (charFunction 2 Nat.eqb v (car (cdr input))) (charFunction 2 Nat.eqb input output) (switchPR (codeIn (car (cdr input)) (codeFreeVarTerm s)) (let nv := codeNewVar (S (cPair v (codeApp (codeFreeVarTerm s) (codeFreeVarFormula (cdr (cdr input)))))) in charFunction 0 (Nat.eqb output (cPair 3 (cPair nv (cTriplePi2 (cdr rest)))) && (Nat.eqb (cTriple v s (cTriplePi2 (car rest))) (cTriplePi1 (cdr rest)) && Nat.eqb (cTriple (car (cdr input)) (cPair 0 nv) (cdr (cdr input))) (cTriplePi1 (car rest)))) * (codeNth (trace - S (car rest)) recs * codeNth (trace - S (cdr rest)) recs)) (charFunction 0 (Nat.eqb output (cPair 3 (cPair (car (cdr input)) (cTriplePi2 rest))) && Nat.eqb (cTriple v s (cdr (cdr input))) (cTriplePi1 rest)) * codeNth (trace - S rest) recs)))) (charFunction 0 (Nat.eqb output (cPair 2 (cTriplePi2 rest)) && Nat.eqb (cTriple v s (cdr input)) (cTriplePi1 rest)) * codeNth (trace - S rest) recs)) (charFunction 0 (Nat.eqb output (cPair 1 (cPair (cTriplePi2 (car rest)) (cTriplePi2 (cdr rest)))) && (Nat.eqb (cTriple v s (car (cdr input))) (cTriplePi1 (car rest)) && Nat.eqb (cTriple v s (cdr (cdr input))) (cTriplePi1 (cdr rest)))) * (codeNth (trace - S (car rest)) recs * codeNth (trace - S (cdr rest)) recs))) (charFunction 2 Nat.eqb output (cPair 0 (cPair (codeSubTerm (car (cdr input)) v s) (codeSubTerm (cdr (cdr input)) v s))))).
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)