DISP	formula_rank_df	==
ABS	formula_rank	== (letrec formula_rank f = case f: x 0; p (formula_rank p + 1); pq ((formula_rank p + formula_rank q) + 1); pq ((formula_rank p + formula_rank q) + 1); pq ((formula_rank p + formula_rank q) + 1); )
ML	formula_rank_unroll	let formula_rankC = (AllC [UnfoldC `formula_rank`; letrec_unrollC; ReduceC; TryC (FoldC `formula_rank`)]) ;; let formula_rank_unrollC = FirstC [FwdMacroC `formula_rank_unrollC` formula_rankC x; FwdMacroC `formula_rank_unrollC` formula_rankC P; FwdMacroC `formula_rank_unrollC` formula_rankC PQ; FwdMacroC `formula_rank_unrollC` formula_rankC PQ; FwdMacroC `formula_rank_unrollC` formula_rankC PQ] ;; add_AbReduce_conv `formula_rank` formula_rank_unrollC ;;
THM	formula_rank_wf	Formula
ML	formula_ind_tac	let FormulaWFInd i = InvImageInd1 CompNatInd i ;;
ML	FormulaRank	let ElimRankAntecedent i = (\p. let i = get_pos_hyp_num i p in (D i THENA (TryOnAllHyps Thin THEN AbReduce 0 THEN GenConclOnAps THEN SIAuto)) p ) ;; let DWith j i = (\p. (With (mk_var_term (var_of_hyp j p)) (D i) THENA Auto) p) ;; let UnaryOpCase = DWith (-2) (-1) THEN ElimRankAntecedent (-1) ;; let BinaryOpCase = CopyToHyp (-1) (-1) THEN DWith (-4) (-2) THEN ElimRankAntecedent (-1) THEN DWith (-3) (-2) THEN ElimRankAntecedent (-1) ;; let FormulaRankInd i = (\p. (let i = get_pos_hyp_num i p in InvImageInd1 CompNatInd i THENA Auto THEN FormulaCases i THENL [Thin (-1); UnaryOpCase; BinaryOpCase; BinaryOpCase; BinaryOpCase]) p ) ;;

the other theories