[STATEMENT]
lemma boundSummandDest[dest]:
  fixes x  :: name
  and   y  :: name
  and   P' :: pi
  and   P  :: pi

  assumes "<\<nu>x>x{y}.P' \<in> summands P"

  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>x{y}.P' \<in> summands P

goal (1 subgoal):
 1. False
[PROOF STEP]
by(induct P rule: pi.induct, auto simp add: if_split pi.inject name_abs_eq name_calc)


[STATEMENT]
lemma summandFresh:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "P \<in> summands Q"
  and     "x \<sharp> Q"

  shows "x \<sharp> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<in> summands Q
x \<sharp> Q

goal (1 subgoal):
 1. x \<sharp> P
[PROOF STEP]
by(nominal_induct Q avoiding: P rule: pi.strong_induct, auto simp add: if_split)


[STATEMENT]
lemma hnfInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "hnf (a<x>.P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hnf (a<x>.P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hnf (a<x>.P)
[PROOF STEP]
obtain y where yineqa: "y \<noteq> a" and yFreshP: "y \<sharp> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> a; y \<sharp> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
y \<noteq> a
y \<sharp> P

goal (1 subgoal):
 1. hnf (a<x>.P)
[PROOF STEP]
from yFreshP
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> P
[PROOF STEP]
have "a<x>.P = a<y>.([(x, y)] \<bullet> P)"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> P

goal (1 subgoal):
 1. a<x>.P = a<y>.([(x, y)] \<bullet> P)
[PROOF STEP]
by(simp add: alphaInput)
[PROOF STATE]
proof (state)
this:
a<x>.P = a<y>.([(x, y)] \<bullet> P)

goal (1 subgoal):
 1. hnf (a<x>.P)
[PROOF STEP]
with yineqa
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> a
a<x>.P = a<y>.([(x, y)] \<bullet> P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a
a<x>.P = a<y>.([(x, y)] \<bullet> P)

goal (1 subgoal):
 1. hnf (a<x>.P)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hnf (a<x>.P)

goal:
No subgoals!
[PROOF STEP]
qed