Theorem: SatStress.t4 (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
x1111 x1110 : Bool
x✝¹¹ : (x1110 && x1111) = x111
x1101 x1100 : Bool
x✝¹⁰ : (x1100 && x1101) = x110
x101 x100 : Bool
x✝⁹ : (x100 && x101) = x10
x1011 x1010 : Bool
x✝⁸ : (x1010 && x1011) = x101
x1001 x1000 : Bool
x✝⁷ : (x1000 && x1001) = x100
x01 x00 : Bool
x✝⁶ : (x00 && x01) = x0
x011 x010 : Bool
x✝⁵ : (x010 && x011) = x01
x0111 x0110 : Bool
x✝⁴ : (x0110 && x0111) = x011
x0101 x0100 : Bool
x✝³ : (x0100 && x0101) = x010
x001 x000 : Bool
x✝² : (x000 && x001) = x00
x0011 x0010 : Bool
x✝¹ : (x0010 && x0011) = x001
x0001 x0000 : Bool
x✝ : (x0000 && x0001) = x000
⊢ x0000 = true
Tactic:
bv_decide
State after:
no goals