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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
⊢ prop
Tactic:
match h:aig.decls[start]'hstart with
| .const b => apply hconst; assumption
| .atom a => apply hatom; assumption
| .gate lhs rhs linv rinv => apply hgate; assumption
State after:
no goals

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

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

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

case b
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
b : Bool
h : aig.decls[start] = Decl.const b
⊢ Bool
Tactic:
assumption
State after:
no goals

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

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

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

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
a : α
h : aig.decls[start] = Decl.atom a
⊢ α
Tactic:
assumption
State after:
no goals

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

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

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

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

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

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

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

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

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

case rinv
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
aig : AIG α
hstart : start < aig.decls.size
prop : Prop
hconst : ∀ (b : Bool), aig.decls[start] = Decl.const b → prop
hatom : ∀ (a : α), aig.decls[start] = Decl.atom a → prop
hgate : ∀ (lhs rhs : Nat) (linv rinv : Bool), aig.decls[start] = Decl.gate lhs rhs linv rinv → prop
lhs rhs : Nat
linv rinv : Bool
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ Bool
Tactic:
assumption
State after:
no goals