[STATEMENT]
lemma (in lbv) merge_pres:
  assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
  shows "merge c pc ss x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
from s0
[PROOF STATE]
proof (chain)
picking this:
snd ` set ss \<subseteq> A
[PROOF STEP]
have "set (map snd [(p', t') \<leftarrow> ss . p'=pc+1]) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
snd ` set ss \<subseteq> A

goal (1 subgoal):
 1. set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A

goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
with x semilat Semilat_axioms
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
semilat (A, r, f)
Semilat A r f
set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A
[PROOF STEP]
have "(map snd [(p', t') \<leftarrow> ss . p'=pc+1] \<Squnion>\<^bsub>f\<^esub> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
semilat (A, r, f)
Semilat A r f
set (map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss)) \<subseteq> A

goal (1 subgoal):
 1. map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A
[PROOF STEP]
by (auto intro!: plusplus_closed)
[PROOF STATE]
proof (state)
this:
map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A

goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
with s0 x
[PROOF STATE]
proof (chain)
picking this:
snd ` set ss \<subseteq> A
x \<in> A
map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
snd ` set ss \<subseteq> A
x \<in> A
map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss) \<Squnion>\<^bsub>f\<^esub> x \<in> A

goal (1 subgoal):
 1. merge c pc ss x \<in> A
[PROOF STEP]
by (simp add: merge_def T_A)
[PROOF STATE]
proof (state)
this:
merge c pc ss x \<in> A

goal:
No subgoals!
[PROOF STEP]
qed