Proof

Proof Summary of Message.thy:771

Isabelle Statement

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

Lemma

lemma MPair_synth_analz [iff]:
     "(⦃X,Y⦄ ∈ synth (analz H)) =  
      (X ∈ synth (analz H) & Y ∈ synth (analz H))"

Proof Excerpt

lemma MPair_synth_analz [iff]:
     "(⦃X,Y⦄ ∈ synth (analz H)) =  
      (X ∈ synth (analz H) & Y ∈ synth (analz H))"
by blast

Conjectures

c_0_1

( ( member_msg @ ( mPair @ x @ y ) @ ( synth @ ( analz @ h ) ) )
  <=> ( ( member_msg @ x @ ( synth @ ( analz @ h ) ) )
  & ( member_msg @ y @ ( synth @ ( analz @ h ) ) ) ) )

Axioms

c_0_0 c_0_2 c_0_3 c_0_4 c_0_5

Final Contradiction

c_0_50