-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.induct_unfolding : ∀ {n : ℕ} (proof : Array Std.Tactic.BVDecide.LRAT.IntAction)
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → ℕ → Std.Tactic.BVDecide.LRAT.Internal.Result → Prop),
  (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
      have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
      step = none →
        motive f (idx + 1) (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1)) →
          motive f idx (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1))) →
    (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
        have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
        ∀ (id : ℕ) (rupHints : Array ℕ),
          step = some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) →
            ∀ (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
              Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f Std.Tactic.BVDecide.LRAT.Internal.Clause.empty
                    rupHints =
                  (fst, true) →
                motive f idx Std.Tactic.BVDecide.LRAT.Internal.Result.success) →
      (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
          have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
          ∀ (id : ℕ) (rupHints : Array ℕ),
            step = some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) →
              ∀ (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (checkSuccess : Bool),
                Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f Std.Tactic.BVDecide.LRAT.Internal.Clause.empty
                      rupHints =
                    (fst, checkSuccess) →
                  ¬checkSuccess = true → motive f idx Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure) →
        (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
            have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
            ∀ (id : ℕ) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ),
              step = some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) →
                ∀ (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
                  Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (fst, true) →
                    motive fst (idx + 1) (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go fst proof (idx + 1)) →
                      motive f idx (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go fst proof (idx + 1))) →
          (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
              have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
              ∀ (id : ℕ) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ),
                step = some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) →
                  ∀ (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (checkSuccess : Bool),
                    Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (fst, checkSuccess) →
                      ¬checkSuccess = true → motive f idx Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure) →
            (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
                have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
                ∀ (id : ℕ) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
                  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
                  (ratHints : Array (ℕ × Array ℕ)),
                  step = some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) →
                    pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
                      ∀ (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
                        Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c pivot rupHints ratHints =
                            (fst, true) →
                          motive fst (idx + 1)
                              (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go fst proof (idx + 1)) →
                            motive f idx
                              (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go fst proof (idx + 1))) →
              (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
                  have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
                  ∀ (id : ℕ) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
                    (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
                    (ratHints : Array (ℕ × Array ℕ)),
                    step = some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) →
                      pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
                        ∀ (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (checkSuccess : Bool),
                          Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c pivot rupHints ratHints =
                              (fst, checkSuccess) →
                            ¬checkSuccess = true → motive f idx Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure) →
                (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
                    have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
                    ∀ (id : ℕ) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
                      (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
                      (ratHints : Array (ℕ × Array ℕ)),
                      step = some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) →
                        pivot ∉ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
                          motive f (idx + 1)
                              (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1)) →
                            motive f idx (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1))) →
                  (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ) (h : idx < proof.size),
                      have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
                      ∀ (ids : Array ℕ),
                        step = some (Std.Tactic.BVDecide.LRAT.Action.del ids) →
                          motive (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids) (idx + 1)
                              (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go
                                (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids) proof (idx + 1)) →
                            motive f idx
                              (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go
                                (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids) proof (idx + 1))) →
                    (∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ),
                        ¬idx < proof.size → motive f idx Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof) →
                      ∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (idx : ℕ),
                        motive f idx (Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof idx)