Theorem: SatStress.t7 (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
x111111 x111110 : Bool
x✝¹²¹ : (x111110 && x111111) = x11111
x1111111 x1111110 : Bool
x✝¹²⁰ : (x1111110 && x1111111) = x111111
x1111101 x1111100 : Bool
x✝¹¹⁹ : (x1111100 && x1111101) = x111110
x111101 x111100 : Bool
x✝¹¹⁸ : (x111100 && x111101) = x11110
x1111011 x1111010 : Bool
x✝¹¹⁷ : (x1111010 && x1111011) = x111101
x1111001 x1111000 : Bool
x✝¹¹⁶ : (x1111000 && x1111001) = x111100
x11101 x11100 : Bool
x✝¹¹⁵ : (x11100 && x11101) = x1110
x111011 x111010 : Bool
x✝¹¹⁴ : (x111010 && x111011) = x11101
x1110111 x1110110 : Bool
x✝¹¹³ : (x1110110 && x1110111) = x111011
x1110101 x1110100 : Bool
x✝¹¹² : (x1110100 && x1110101) = x111010
x111001 x111000 : Bool
x✝¹¹¹ : (x111000 && x111001) = x11100
x1110011 x1110010 : Bool
x✝¹¹⁰ : (x1110010 && x1110011) = x111001
x1110001 x1110000 : Bool
x✝¹⁰⁹ : (x1110000 && x1110001) = x111000
x1101 x1100 : Bool
x✝¹⁰⁸ : (x1100 && x1101) = x110
x11011 x11010 : Bool
x✝¹⁰⁷ : (x11010 && x11011) = x1101
x110111 x110110 : Bool
x✝¹⁰⁶ : (x110110 && x110111) = x11011
x1101111 x1101110 : Bool
x✝¹⁰⁵ : (x1101110 && x1101111) = x110111
x1101101 x1101100 : Bool
x✝¹⁰⁴ : (x1101100 && x1101101) = x110110
x110101 x110100 : Bool
x✝¹⁰³ : (x110100 && x110101) = x11010
x1101011 x1101010 : Bool
x✝¹⁰² : (x1101010 && x1101011) = x110101
x1101001 x1101000 : Bool
x✝¹⁰¹ : (x1101000 && x1101001) = x110100
x11001 x11000 : Bool
x✝¹⁰⁰ : (x11000 && x11001) = x1100
x110011 x110010 : Bool
x✝⁹⁹ : (x110010 && x110011) = x11001
x1100111 x1100110 : Bool
x✝⁹⁸ : (x1100110 && x1100111) = x110011
x1100101 x1100100 : Bool
x✝⁹⁷ : (x1100100 && x1100101) = x110010
x110001 x110000 : Bool
x✝⁹⁶ : (x110000 && x110001) = x11000
x1100011 x1100010 : Bool
x✝⁹⁵ : (x1100010 && x1100011) = x110001
x1100001 x1100000 : Bool
x✝⁹⁴ : (x1100000 && x1100001) = x110000
x101 x100 : Bool
x✝⁹³ : (x100 && x101) = x10
x1011 x1010 : Bool
x✝⁹² : (x1010 && x1011) = x101
x10111 x10110 : Bool
x✝⁹¹ : (x10110 && x10111) = x1011
x101111 x101110 : Bool
x✝⁹⁰ : (x101110 && x101111) = x10111
x1011111 x1011110 : Bool
x✝⁸⁹ : (x1011110 && x1011111) = x101111
x1011101 x1011100 : Bool
x✝⁸⁸ : (x1011100 && x1011101) = x101110
x101101 x101100 : Bool
x✝⁸⁷ : (x101100 && x101101) = x10110
x1011011 x1011010 : Bool
x✝⁸⁶ : (x1011010 && x1011011) = x101101
x1011001 x1011000 : Bool
x✝⁸⁵ : (x1011000 && x1011001) = x101100
x10101 x10100 : Bool
x✝⁸⁴ : (x10100 && x10101) = x1010
x101011 x101010 : Bool
x✝⁸³ : (x101010 && x101011) = x10101
x1010111 x1010110 : Bool
x✝⁸² : (x1010110 && x1010111) = x101011
x1010101 x1010100 : Bool
x✝⁸¹ : (x1010100 && x1010101) = x101010
x101001 x101000 : Bool
x✝⁸⁰ : (x101000 && x101001) = x10100
x1010011 x1010010 : Bool
x✝⁷⁹ : (x1010010 && x1010011) = x101001
x1010001 x1010000 : Bool
x✝⁷⁸ : (x1010000 && x1010001) = x101000
x1001 x1000 : Bool
x✝⁷⁷ : (x1000 && x1001) = x100
x10011 x10010 : Bool
x✝⁷⁶ : (x10010 && x10011) = x1001
x100111 x100110 : Bool
x✝⁷⁵ : (x100110 && x100111) = x10011
x1001111 x1001110 : Bool
x✝⁷⁴ : (x1001110 && x1001111) = x100111
x1001101 x1001100 : Bool
x✝⁷³ : (x1001100 && x1001101) = x100110
x100101 x100100 : Bool
x✝⁷² : (x100100 && x100101) = x10010
x1001011 x1001010 : Bool
x✝⁷¹ : (x1001010 && x1001011) = x100101
x1001001 x1001000 : Bool
x✝⁷⁰ : (x1001000 && x1001001) = x100100
x10001 x10000 : Bool
x✝⁶⁹ : (x10000 && x10001) = x1000
x100011 x100010 : Bool
x✝⁶⁸ : (x100010 && x100011) = x10001
x1000111 x1000110 : Bool
x✝⁶⁷ : (x1000110 && x1000111) = x100011
x1000101 x1000100 : Bool
x✝⁶⁶ : (x1000100 && x1000101) = x100010
x100001 x100000 : Bool
x✝⁶⁵ : (x100000 && x100001) = x10000
x1000011 x1000010 : Bool
x✝⁶⁴ : (x1000010 && x1000011) = x100001
x1000001 x1000000 : Bool
x✝⁶³ : (x1000000 && x1000001) = x100000
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
x011111 x011110 : Bool
x✝⁵⁸ : (x011110 && x011111) = x01111
x0111111 x0111110 : Bool
x✝⁵⁷ : (x0111110 && x0111111) = x011111
x0111101 x0111100 : Bool
x✝⁵⁶ : (x0111100 && x0111101) = x011110
x011101 x011100 : Bool
x✝⁵⁵ : (x011100 && x011101) = x01110
x0111011 x0111010 : Bool
x✝⁵⁴ : (x0111010 && x0111011) = x011101
x0111001 x0111000 : Bool
x✝⁵³ : (x0111000 && x0111001) = x011100
x01101 x01100 : Bool
x✝⁵² : (x01100 && x01101) = x0110
x011011 x011010 : Bool
x✝⁵¹ : (x011010 && x011011) = x01101
x0110111 x0110110 : Bool
x✝⁵⁰ : (x0110110 && x0110111) = x011011
x0110101 x0110100 : Bool
x✝⁴⁹ : (x0110100 && x0110101) = x011010
x011001 x011000 : Bool
x✝⁴⁸ : (x011000 && x011001) = x01100
x0110011 x0110010 : Bool
x✝⁴⁷ : (x0110010 && x0110011) = x011001
x0110001 x0110000 : Bool
x✝⁴⁶ : (x0110000 && x0110001) = x011000
x0101 x0100 : Bool
x✝⁴⁵ : (x0100 && x0101) = x010
x01011 x01010 : Bool
x✝⁴⁴ : (x01010 && x01011) = x0101
x010111 x010110 : Bool
x✝⁴³ : (x010110 && x010111) = x01011
x0101111 x0101110 : Bool
x✝⁴² : (x0101110 && x0101111) = x010111
x0101101 x0101100 : Bool
x✝⁴¹ : (x0101100 && x0101101) = x010110
x010101 x010100 : Bool
x✝⁴⁰ : (x010100 && x010101) = x01010
x0101011 x0101010 : Bool
x✝³⁹ : (x0101010 && x0101011) = x010101
x0101001 x0101000 : Bool
x✝³⁸ : (x0101000 && x0101001) = x010100
x01001 x01000 : Bool
x✝³⁷ : (x01000 && x01001) = x0100
x010011 x010010 : Bool
x✝³⁶ : (x010010 && x010011) = x01001
x0100111 x0100110 : Bool
x✝³⁵ : (x0100110 && x0100111) = x010011
x0100101 x0100100 : Bool
x✝³⁴ : (x0100100 && x0100101) = x010010
x010001 x010000 : Bool
x✝³³ : (x010000 && x010001) = x01000
x0100011 x0100010 : Bool
x✝³² : (x0100010 && x0100011) = x010001
x0100001 x0100000 : Bool
x✝³¹ : (x0100000 && x0100001) = x010000
x001 x000 : Bool
x✝³⁰ : (x000 && x001) = x00
x0011 x0010 : Bool
x✝²⁹ : (x0010 && x0011) = x001
x00111 x00110 : Bool
x✝²⁸ : (x00110 && x00111) = x0011
x001111 x001110 : Bool
x✝²⁷ : (x001110 && x001111) = x00111
x0011111 x0011110 : Bool
x✝²⁶ : (x0011110 && x0011111) = x001111
x0011101 x0011100 : Bool
x✝²⁵ : (x0011100 && x0011101) = x001110
x001101 x001100 : Bool
x✝²⁴ : (x001100 && x001101) = x00110
x0011011 x0011010 : Bool
x✝²³ : (x0011010 && x0011011) = x001101
x0011001 x0011000 : Bool
x✝²² : (x0011000 && x0011001) = x001100
x00101 x00100 : Bool
x✝²¹ : (x00100 && x00101) = x0010
x001011 x001010 : Bool
x✝²⁰ : (x001010 && x001011) = x00101
x0010111 x0010110 : Bool
x✝¹⁹ : (x0010110 && x0010111) = x001011
x0010101 x0010100 : Bool
x✝¹⁸ : (x0010100 && x0010101) = x001010
x001001 x001000 : Bool
x✝¹⁷ : (x001000 && x001001) = x00100
x0010011 x0010010 : Bool
x✝¹⁶ : (x0010010 && x0010011) = x001001
x0010001 x0010000 : Bool
x✝¹⁵ : (x0010000 && x0010001) = x001000
x0001 x0000 : Bool
x✝¹⁴ : (x0000 && x0001) = x000
x00011 x00010 : Bool
x✝¹³ : (x00010 && x00011) = x0001
x000111 x000110 : Bool
x✝¹² : (x000110 && x000111) = x00011
x0001111 x0001110 : Bool
x✝¹¹ : (x0001110 && x0001111) = x000111
x0001101 x0001100 : Bool
x✝¹⁰ : (x0001100 && x0001101) = x000110
x000101 x000100 : Bool
x✝⁹ : (x000100 && x000101) = x00010
x0001011 x0001010 : Bool
x✝⁸ : (x0001010 && x0001011) = x000101
x0001001 x0001000 : Bool
x✝⁷ : (x0001000 && x0001001) = x000100
x00001 x00000 : Bool
x✝⁶ : (x00000 && x00001) = x0000
x000011 x000010 : Bool
x✝⁵ : (x000010 && x000011) = x00001
x0000111 x0000110 : Bool
x✝⁴ : (x0000110 && x0000111) = x000011
x0000101 x0000100 : Bool
x✝³ : (x0000100 && x0000101) = x000010
x000001 x000000 : Bool
x✝² : (x000000 && x000001) = x00000
x0000011 x0000010 : Bool
x✝¹ : (x0000010 && x0000011) = x000001
x0000001 x0000000 : Bool
x✝ : (x0000000 && x0000001) = x000000
⊢ x0000000 = true
Tactic:
bv_decide
State after:
no goals