[STATEMENT]
lemma (in append_impl)
  shows
   "\<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>\<^sub>t
      \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and>  List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<rbrace>
       \<acute>p :== PROC append(\<acute>p,\<acute>q)
      \<lbrace>List \<acute>p \<acute>next (Ps@Qs) \<and> (\<forall>x. x\<notin>set Ps \<longrightarrow> \<acute>next x = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>\<^sub>t \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace> \<acute>p :== PROC append(\<acute>p,\<acute>q) \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>
[PROOF STEP]
apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (\<lambda>(s,p). length (list \<^bsup>s\<^esup>p \<^bsup>s\<^esup>next))"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> \<sigma>' Ps Qs. \<Gamma>,(\<Union>\<sigma>' Ps Qs. {(\<lbrace>\<sigma>'. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace> \<inter> \<lbrace>length (list \<acute>p \<acute>next) < length (list \<^bsup>\<sigma>\<^esup>p \<^bsup>\<sigma>\<^esup>next)\<rbrace>, append_'proc, \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>'\<^esup>next x)\<rbrace>, {})})\<turnstile>\<^sub>t ({\<sigma>} \<inter> \<lbrace>\<sigma>'. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace>) IF \<acute>p = Null THEN \<acute>p :== \<acute>q ELSE \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p\<rightarrow>\<acute>next,\<acute>q) FI \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>'\<^esup>next x)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps Qs next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> List q next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> next x = next x)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>Psa. List (next p) next Psa \<and> (\<exists>Qsa. List q next Qsa \<and> set Psa \<inter> set Qsa = {} \<and> length (list (next p) next) < length (list p next) \<and> (\<forall>nexta pa. List pa nexta (Psa @ Qsa) \<and> (\<forall>x. x \<notin> set Psa \<longrightarrow> nexta x = next x) \<longrightarrow> List p (nexta(p := pa)) (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> (nexta(p := pa)) x = next x)))))
[PROOF STEP]
apply (fastforce  simp add: List_list)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done