Proof

Proof Summary of Message.thy:138

Isabelle Statement

source: Message.thy:138 benchmark: isa/deeper/B-mesh-th0/train2k problem: problems/Tutorial/0035_Message/prob_00138_003649.p

Lemma

lemma keysFor_empty [simp]: "keysFor {} = {}"

Proof Excerpt

lemma keysFor_empty [simp]: "keysFor {} = {}"
by (unfold keysFor_def, blast)

Conjectures

c_0_6

( ( keysFor @ bot_bot_set_msg )
= bot_bot_set_nat )

Axioms

c_0_0 c_0_1 c_0_2 c_0_3 c_0_4 c_0_5

Final Contradiction

c_0_41