Theorem: AIG.denote_idx_trichotomy (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
apply idx_trichotomy aig hstart
State after:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

State before:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
. exact hconst
State after:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

State before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
. exact hatom
State after:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res

State before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
. exact hgate
State after:
no goals

State before:
case hconst
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
exact hconst
State after:
no goals

State before:
case hatom
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
exact hatom
State after:
no goals

State before:
case hgate
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
res : Bool
aig : AIG α
hstart : start < aig.decls.size
hconst :
  ∀ (b : Bool),
    aig.decls[start] = Decl.const b → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hatom :
  ∀ (a : α), aig.decls[start] = Decl.atom a → ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
hgate :
  ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    aig.decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = res
Tactic:
exact hgate
State after:
no goals