[STATEMENT]
lemma eeqButPID_update_post:
assumes "eeqButPID ntcs ntcs1"
shows "eeqButPID (ntcs (pid := ntc)) (ntcs1 (pid := ntc))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqButPID (ntcs(pid := ntc)) (ntcs1(pid := ntc))
[PROOF STEP]
using eeqButPID_not_PID[OF assms]
[PROOF STATE]
proof (prove)
using this:
?pid \<noteq> PID \<Longrightarrow> ntcs ?pid = ntcs1 ?pid

goal (1 subgoal):
 1. eeqButPID (ntcs(pid := ntc)) (ntcs1(pid := ntc))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?pid \<noteq> PID \<Longrightarrow> ntcs ?pid = ntcs1 ?pid
eeqButPID ntcs ntcs1

goal (1 subgoal):
 1. eeqButPID (ntcs(pid := ntc)) (ntcs1(pid := ntc))
[PROOF STEP]
unfolding eeqButPID_def
[PROOF STATE]
proof (prove)
using this:
?pid \<noteq> PID \<Longrightarrow> ntcs ?pid = ntcs1 ?pid
\<forall>pid. pid \<noteq> PID \<longrightarrow> ntcs pid = ntcs1 pid

goal (1 subgoal):
 1. \<forall>pida. pida \<noteq> PID \<longrightarrow> (ntcs(pid := ntc)) pida = (ntcs1(pid := ntc)) pida
[PROOF STEP]
by auto