Theorem: SatStress.t3 (Test/Bv/SatStress.lean)

State before:
x : Bool
x✝⁷ : x = true
x1 x0 : Bool
x✝⁶ : (x0 && x1) = x
x11 x10 : Bool
x✝⁵ : (x10 && x11) = x1
x111 x110 : Bool
x✝⁴ : (x110 && x111) = x11
x101 x100 : Bool
x✝³ : (x100 && x101) = x10
x01 x00 : Bool
x✝² : (x00 && x01) = x0
x011 x010 : Bool
x✝¹ : (x010 && x011) = x01
x001 x000 : Bool
x✝ : (x000 && x001) = x00
⊢ x000 = true
Tactic:
bv_decide
State after:
no goals