[STATEMENT]
lemma and_or_s: 
assumes "(((get_S w1))::word1) = 0 \<and> 
  (AND) w2 (0b00000000000000000000000010000000::word32) = 0"
shows "(((get_S ((OR) ((AND) w1 
  (0b11111111000011111111111111111111::word32)) w2)))::word1) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
get_S w1 = 0 \<and> w2 AND 128 = 0
[PROOF STEP]
have "w1 AND 128 = 0"
[PROOF STATE]
proof (prove)
using this:
get_S w1 = 0 \<and> w2 AND 128 = 0

goal (1 subgoal):
 1. w1 AND 128 = 0
[PROOF STEP]
using ucast_s
[PROOF STATE]
proof (prove)
using this:
get_S w1 = 0 \<and> w2 AND 128 = 0
get_S ?w = 0 \<Longrightarrow> ?w AND 128 = 0

goal (1 subgoal):
 1. w1 AND 128 = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w1 AND 128 = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w1 AND 128 = 0
[PROOF STEP]
have "(w1 AND 4279238655 OR w2) AND 128 = 0"
[PROOF STATE]
proof (prove)
using this:
w1 AND 128 = 0

goal (1 subgoal):
 1. (w1 AND 4279238655 OR w2) AND 128 = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w1 AND 128 = 0
get_S w1 = 0 \<and> w2 AND 128 = 0

goal (1 subgoal):
 1. (w1 AND 4279238655 OR w2) AND 128 = 0
[PROOF STEP]
by (metis word_ao_absorbs(6) word_ao_dist word_bw_comms(2))
[PROOF STATE]
proof (state)
this:
(w1 AND 4279238655 OR w2) AND 128 = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(w1 AND 4279238655 OR w2) AND 128 = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(w1 AND 4279238655 OR w2) AND 128 = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
using ucast_s2
[PROOF STATE]
proof (prove)
using this:
(w1 AND 4279238655 OR w2) AND 128 = 0
?w AND 128 = 0 \<Longrightarrow> get_S ?w = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_S (w1 AND 4279238655 OR w2) = 0

goal:
No subgoals!
[PROOF STEP]
qed