Theorem: SatStress.t5 (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
x11111 x11110 : Bool
x✝²⁶ : (x11110 && x11111) = x1111
x11101 x11100 : Bool
x✝²⁵ : (x11100 && x11101) = x1110
x1101 x1100 : Bool
x✝²⁴ : (x1100 && x1101) = x110
x11011 x11010 : Bool
x✝²³ : (x11010 && x11011) = x1101
x11001 x11000 : Bool
x✝²² : (x11000 && x11001) = x1100
x101 x100 : Bool
x✝²¹ : (x100 && x101) = x10
x1011 x1010 : Bool
x✝²⁰ : (x1010 && x1011) = x101
x10111 x10110 : Bool
x✝¹⁹ : (x10110 && x10111) = x1011
x10101 x10100 : Bool
x✝¹⁸ : (x10100 && x10101) = x1010
x1001 x1000 : Bool
x✝¹⁷ : (x1000 && x1001) = x100
x10011 x10010 : Bool
x✝¹⁶ : (x10010 && x10011) = x1001
x10001 x10000 : Bool
x✝¹⁵ : (x10000 && x10001) = x1000
x01 x00 : Bool
x✝¹⁴ : (x00 && x01) = x0
x011 x010 : Bool
x✝¹³ : (x010 && x011) = x01
x0111 x0110 : Bool
x✝¹² : (x0110 && x0111) = x011
x01111 x01110 : Bool
x✝¹¹ : (x01110 && x01111) = x0111
x01101 x01100 : Bool
x✝¹⁰ : (x01100 && x01101) = x0110
x0101 x0100 : Bool
x✝⁹ : (x0100 && x0101) = x010
x01011 x01010 : Bool
x✝⁸ : (x01010 && x01011) = x0101
x01001 x01000 : Bool
x✝⁷ : (x01000 && x01001) = x0100
x001 x000 : Bool
x✝⁶ : (x000 && x001) = x00
x0011 x0010 : Bool
x✝⁵ : (x0010 && x0011) = x001
x00111 x00110 : Bool
x✝⁴ : (x00110 && x00111) = x0011
x00101 x00100 : Bool
x✝³ : (x00100 && x00101) = x0010
x0001 x0000 : Bool
x✝² : (x0000 && x0001) = x000
x00011 x00010 : Bool
x✝¹ : (x00010 && x00011) = x0001
x00001 x00000 : Bool
x✝ : (x00000 && x00001) = x0000
⊢ x00000 = true
Tactic:
bv_decide
State after:
no goals