Theorem: BVDecide.verifyCert_correct
Proof state before:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
⊢ ∀
    (a :
      LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1))
        (PosFin ((LratFormula.ofCnf c).numVars + 1))),
    a ∈
        List.map Subtype.val
          (List.filterMap
            (fun actOpt =>
              match actOpt with
              | none => none
              | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
              | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
              | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
              | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                else none)
            (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList)) →
      LRAT.wellFormedAction a
Tactic:
intro action h
Proof state after:
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  LRAT.lratChecker (LratFormula.ofCnf c).formula
      (List.map Subtype.val
        (List.filterMap
          (fun actOpt =>
            match actOpt with
            | none => none
            | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
            | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
            | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
            | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
              if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
              else none)
          (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))) =
    LRAT.Result.success
action :
  LRAT.Action (LRAT.DefaultClause ((LratFormula.ofCnf c).numVars + 1)) (PosFin ((LratFormula.ofCnf c).numVars + 1))
h :
  action ∈
    List.map Subtype.val
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
          | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
          | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
          | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
            if h : pivot ∈ LRAT.Clause.toList c_1 then some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
            else none)
        (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1)) lratProof✝.toList))
⊢ LRAT.wellFormedAction action