theory CNodeInv_AI

lemma decode_cnode_cases2:
  assumes mvins: "\<And>index bits src_index src_depth args' src_root_cap exs'.
                    \<lbrakk> args = index # bits # src_index # src_depth # args';
                      exs = src_root_cap # exs';
                      gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate];
                      gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller];
                      gen_invocation_type label \<notin> {CNodeRevoke, CNodeDelete,
                      CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller} \<rbrakk> \<Longrightarrow> P"
  assumes rvk: "\<And>index bits args'. \<lbrakk> args = index # bits # args';
                          gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate];
                          gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller];
                          gen_invocation_type label = CNodeRevoke \<rbrakk> \<Longrightarrow> P"
  assumes dlt: "\<And>index bits args'. \<lbrakk> args = index # bits # args';
                          gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate];
                          gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller];
                          gen_invocation_type label = CNodeDelete \<rbrakk> \<Longrightarrow> P"
  assumes svc: "\<And>index bits args'. \<lbrakk> args = index # bits # args';
                          gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate];
                          gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller];
                          gen_invocation_type label = CNodeSaveCaller \<rbrakk> \<Longrightarrow> P"
  assumes rcy: "\<And>index bits args'. \<lbrakk> args = index # bits # args';
                          gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate];
                          gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller];
                          gen_invocation_type label = CNodeCancelBadgedSends \<rbrakk> \<Longrightarrow> P"
  assumes rot: "\<And>index bits pivot_new_data pivot_index pivot_depth src_new_data
                  src_index src_depth args' pivot_root_cap src_root_cap exs'.
                     \<lbrakk> args = index # bits # pivot_new_data # pivot_index # pivot_depth
                                 # src_new_data # src_index # src_depth # args';
                       exs = pivot_root_cap # src_root_cap # exs';
                       gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate];
                       gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller];
                       gen_invocation_type label = CNodeRotate \<rbrakk> \<Longrightarrow> P"
  assumes errs:
      "\<lbrakk> gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or>
         args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and>
                             gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and>
                             (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]
                                        \<and> gen_invocation_type label \<notin> {CNodeRevoke, CNodeDelete,
                                             CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller}
                                        \<and> (case (args', exs) of (src_index # src_depth # args'',
                                                    src_root_cap # exs') \<Rightarrow> False | _ \<Rightarrow> True) \<or>
                              gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and>
                              gen_invocation_type label = CNodeRotate \<and> (case (args', exs) of
                              (pivot_new_data # pivot_index # pivot_depth
                                 # src_new_data # src_index # src_depth # args'',
                               pivot_root_cap # src_root_cap # exs') \<Rightarrow> False
                                         | _ \<Rightarrow> True))) \<rbrakk> \<Longrightarrow> P"
  shows "P" proof - have simps: "[CNodeRevoke .e. CNodeSaveCaller]
                     = [CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeCopy, CNodeMint,
                        CNodeMove, CNodeMutate, CNodeRotate, CNodeSaveCaller]"
              "[CNodeCopy .e. CNodeMutate] = [CNodeCopy, CNodeMint,
                        CNodeMove, CNodeMutate]" by (simp_all add: upto_enum_def fromEnum_def toEnum_def enum_invocation_label enum_gen_invocation_labels) show ?thesis apply (cases args) apply (simp add: errs) apply (case_tac list) apply (simp add: errs) apply (case_tac "gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]") apply (case_tac "case (lista, exs) of (src_index # src_depth # args'',
                             src_root_cap # exs'') \<Rightarrow> False | _ \<Rightarrow> True") apply (rule errs) apply (simp add: simps) apply (rule disjI2) apply auto[1] apply (simp split: prod.split_asm list.split_asm) apply (erule(2) mvins, auto simp: simps)[1] apply (case_tac "gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]") apply (simp_all add: errs) apply (insert rvk dlt svc rcy rot) apply (simp add: simps) apply atomize apply (elim disjE, simp_all) apply (case_tac "case (lista, exs) of
                         (pivot_new_data # pivot_index # pivot_depth
                             # src_new_data # src_index # src_depth # args'',
                          pivot_root_cap # src_root_cap # exs') \<Rightarrow> False
                                         | _ \<Rightarrow> True") apply (rule errs) apply (simp add: simps) apply (simp split: prod.split_asm list.split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (state)
goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. [CNodeRevoke .e. CNodeSaveCaller] = [CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeCopy, CNodeMint, CNodeMove, CNodeMutate, CNodeRotate, CNodeSaveCaller] &&& [CNodeCopy .e. CNodeMutate] = [CNodeCopy, CNodeMint, CNodeMove, CNodeMutate] proof (state)
this:
[CNodeRevoke .e. CNodeSaveCaller] = [CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeCopy, CNodeMint, CNodeMove, CNodeMutate, CNodeRotate, CNodeSaveCaller]
[CNodeCopy .e. CNodeMutate] = [CNodeCopy, CNodeMint, CNodeMove, CNodeMutate]

goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. P proof (prove)
goal (2 subgoals):
 1. args = [] \<Longrightarrow> P
 2. \<And>a list. args = a # list \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list. args = a # list \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>args = a # list; list = []\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P
 3. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False\<rbrakk> \<Longrightarrow> gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<notin> {CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller} \<and> (case (args', exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs') \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case (args', exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False)))
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P
 3. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; gen_invocation_type label = CNodeCopy \<or> gen_invocation_type label = CNodeMint \<or> gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate; case lista of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case exs of [] \<Rightarrow> True | src_root_cap # exs'' \<Rightarrow> False\<rbrakk> \<Longrightarrow> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeCopy \<and> gen_invocation_type label \<noteq> CNodeMint \<and> gen_invocation_type label \<noteq> CNodeMove \<and> gen_invocation_type label \<noteq> CNodeMutate \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller \<or> (gen_invocation_type label = CNodeRevoke \<or> gen_invocation_type label = CNodeDelete \<or> gen_invocation_type label = CNodeCancelBadgedSends \<or> gen_invocation_type label = CNodeCopy \<or> gen_invocation_type label = CNodeMint \<or> gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate \<or> gen_invocation_type label = CNodeRotate \<or> gen_invocation_type label = CNodeSaveCaller) \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P
 3. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; gen_invocation_type label = CNodeCopy \<or> gen_invocation_type label = CNodeMint \<or> gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate; case lista of [] \<Rightarrow> True | [src_index] \<Rightarrow> True | src_index # src_depth # args'' \<Rightarrow> case exs of [] \<Rightarrow> True | src_root_cap # exs'' \<Rightarrow> False\<rbrakk> \<Longrightarrow> (gen_invocation_type label = CNodeRevoke \<or> gen_invocation_type label = CNodeDelete \<or> gen_invocation_type label = CNodeCancelBadgedSends \<or> gen_invocation_type label = CNodeCopy \<or> gen_invocation_type label = CNodeMint \<or> gen_invocation_type label = CNodeMove \<or> gen_invocation_type label = CNodeMutate \<or> gen_invocation_type label = CNodeRotate \<or> gen_invocation_type label = CNodeSaveCaller) \<and> gen_invocation_type label \<noteq> CNodeRevoke \<and> gen_invocation_type label \<noteq> CNodeDelete \<and> gen_invocation_type label \<noteq> CNodeCancelBadgedSends \<and> gen_invocation_type label \<noteq> CNodeRotate \<and> gen_invocation_type label \<noteq> CNodeSaveCaller
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P
 3. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs'') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista x21 x22 x21a x22a x21b x22b. \<lbrakk>args = a # aa # x21 # x21a # x22a; list = aa # x21 # x21a # x22a; gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate]; lista = x21 # x21a # x22a; x22 = x21a # x22a; exs = x21b # x22b\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # list; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; \<And>index bits args'. \<lbrakk>args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRevoke\<rbrakk> \<Longrightarrow> P; \<And>index bits args'. \<lbrakk>args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeDelete\<rbrakk> \<Longrightarrow> P; \<And>index bits args'. \<lbrakk>args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> P; \<And>index bits args'. \<lbrakk>args = index # bits # args'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> P; \<And>index bits pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args' pivot_root_cap src_root_cap exs'. \<lbrakk>args = index # bits # pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; exs = pivot_root_cap # src_root_cap # exs'; gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate]; gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller]; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; gen_invocation_type label \<noteq> CNodeCopy \<and> gen_invocation_type label \<noteq> CNodeMint \<and> gen_invocation_type label \<noteq> CNodeMove \<and> gen_invocation_type label \<noteq> CNodeMutate; gen_invocation_type label = CNodeRevoke \<or> gen_invocation_type label = CNodeDelete \<or> gen_invocation_type label = CNodeCancelBadgedSends \<or> gen_invocation_type label = CNodeRotate \<or> gen_invocation_type label = CNodeSaveCaller; gen_invocation_type label = CNodeRevoke \<Longrightarrow> P; gen_invocation_type label = CNodeDelete \<Longrightarrow> P; gen_invocation_type label = CNodeSaveCaller \<Longrightarrow> P; gen_invocation_type label = CNodeCancelBadgedSends \<Longrightarrow> P; \<And>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args' pivot_root_cap src_root_cap exs'. \<lbrakk>lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'; exs = pivot_root_cap # src_root_cap # exs'; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; gen_invocation_type label \<noteq> CNodeCopy \<and> gen_invocation_type label \<noteq> CNodeMint \<and> gen_invocation_type label \<noteq> CNodeMove \<and> gen_invocation_type label \<noteq> CNodeMutate; gen_invocation_type label = CNodeRevoke \<or> gen_invocation_type label = CNodeDelete \<or> gen_invocation_type label = CNodeCancelBadgedSends \<or> gen_invocation_type label = CNodeRotate \<or> gen_invocation_type label = CNodeSaveCaller; gen_invocation_type label = CNodeRevoke \<longrightarrow> P; gen_invocation_type label = CNodeDelete \<longrightarrow> P; gen_invocation_type label = CNodeSaveCaller \<longrightarrow> P; gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> P; \<forall>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args' pivot_root_cap src_root_cap exs'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args' \<longrightarrow> exs = pivot_root_cap # src_root_cap # exs' \<longrightarrow> gen_invocation_type label = CNodeRotate \<longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; (\<exists>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args') \<longrightarrow> (\<exists>pivot_root_cap src_root_cap exs'. exs = pivot_root_cap # src_root_cap # exs') \<longrightarrow> P; gen_invocation_type label = CNodeRotate\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; (\<exists>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args') \<longrightarrow> (\<exists>pivot_root_cap src_root_cap exs'. exs = pivot_root_cap # src_root_cap # exs') \<longrightarrow> P; gen_invocation_type label = CNodeRotate; case (lista, exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False\<rbrakk> \<Longrightarrow> P
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; (\<exists>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args') \<longrightarrow> (\<exists>pivot_root_cap src_root_cap exs'. exs = pivot_root_cap # src_root_cap # exs') \<longrightarrow> P; gen_invocation_type label = CNodeRotate; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; (\<exists>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args') \<longrightarrow> (\<exists>pivot_root_cap src_root_cap exs'. exs = pivot_root_cap # src_root_cap # exs') \<longrightarrow> P; gen_invocation_type label = CNodeRotate; case (lista, exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False\<rbrakk> \<Longrightarrow> gen_invocation_type label \<notin> set [CNodeRevoke .e. CNodeSaveCaller] \<or> args = [] \<or> (\<exists>x. args = [x]) \<or> (\<exists>index bits args'. args = index # bits # args' \<and> gen_invocation_type label \<in> set [CNodeRevoke .e. CNodeSaveCaller] \<and> (gen_invocation_type label \<in> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label \<notin> {CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller} \<and> (case (args', exs) of ([], b) \<Rightarrow> True | ([src_index], b) \<Rightarrow> True | (src_index # src_depth # args'', []) \<Rightarrow> True | (src_index # src_depth # args'', src_root_cap # exs') \<Rightarrow> False) \<or> gen_invocation_type label \<notin> set [CNodeCopy .e. CNodeMutate] \<and> gen_invocation_type label = CNodeRotate \<and> (case (args', exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False)))
 2. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; (\<exists>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args') \<longrightarrow> (\<exists>pivot_root_cap src_root_cap exs'. exs = pivot_root_cap # src_root_cap # exs') \<longrightarrow> P; gen_invocation_type label = CNodeRotate; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>args = a # aa # lista; list = aa # lista; (\<exists>pivot_new_data pivot_index pivot_depth src_new_data src_index src_depth args'. lista = pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args') \<longrightarrow> (\<exists>pivot_root_cap src_root_cap exs'. exs = pivot_root_cap # src_root_cap # exs') \<longrightarrow> P; gen_invocation_type label = CNodeRotate; \<not> (case (lista, exs) of ([], b) \<Rightarrow> True | ([pivot_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data], b) \<Rightarrow> True | ([pivot_new_data, pivot_index, pivot_depth, src_new_data, src_index], b) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', []) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', [pivot_root_cap]) \<Rightarrow> True | (pivot_new_data # pivot_index # pivot_depth # src_new_data # src_index # src_depth # args'', pivot_root_cap # src_root_cap # exs') \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals! proof (state)
this:
P

goal:
No subgoals!