theory StateTranslation_D

lemma transform_intent_isnot_CNodeIntent:
      "(\<not> (\<exists> ui. Some (CNodeIntent ui) = transform_intent label args))
       = ((label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and>
          (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and>
          (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and>
          (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and>
          (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and>
          (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and>
          (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and>
          (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and>
          (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2))" apply(rule iffI) apply(erule contrapos_np) apply(clarsimp simp: transform_intent_def) apply(cases label; simp) apply(rename_tac gen_label, case_tac gen_label;
           simp add: transform_intent_cnode_defs option_map_def
                split: list.split) prefer 10 apply(clarify) apply(case_labels label;
                   clarsimp simp: transform_intent_def option_map_def transform_intent_cnode_defs
                            split: list.split_asm option.split_asm) apply(auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<nexists>ui. Some (CNodeIntent ui) = transform_intent label args) = ((label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2)) proof (prove)
goal (2 subgoals):
 1. \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args \<Longrightarrow> (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2)
 2. (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<not> ((label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2)) \<Longrightarrow> \<exists>ui. Some (CNodeIntent ui) = transform_intent label args
 2. (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. label = GenInvocationLabel CNodeRevoke \<and> \<not> length args < 2 \<or> label = GenInvocationLabel CNodeDelete \<and> \<not> length args < 2 \<or> label = GenInvocationLabel CNodeCancelBadgedSends \<and> \<not> length args < 2 \<or> label = GenInvocationLabel CNodeCopy \<and> \<not> length args < 5 \<or> label = GenInvocationLabel CNodeMint \<and> \<not> length args < 6 \<or> label = GenInvocationLabel CNodeMove \<and> \<not> length args < 4 \<or> label = GenInvocationLabel CNodeMutate \<and> \<not> length args < 5 \<or> label = GenInvocationLabel CNodeRotate \<and> \<not> length args < 8 \<or> label = GenInvocationLabel CNodeSaveCaller \<and> \<not> length args < 2 \<Longrightarrow> \<exists>ui. Some (CNodeIntent ui) = (case label of GenInvocationLabel InvalidInvocation \<Rightarrow> None | GenInvocationLabel UntypedRetype \<Rightarrow> map_option UntypedIntent (transform_intent_untyped_retype args) | GenInvocationLabel TCBReadRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_read_registers args) | GenInvocationLabel TCBWriteRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_write_registers args) | GenInvocationLabel TCBCopyRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_copy_registers args) | GenInvocationLabel TCBConfigure \<Rightarrow> map_option TcbIntent (transform_intent_tcb_configure args) | GenInvocationLabel TCBSetPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_priority args) | GenInvocationLabel TCBSetMCPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_mcpriority args) | GenInvocationLabel TCBSetSchedParams \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_sched_params args) | GenInvocationLabel TCBSetIPCBuffer \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args) | GenInvocationLabel TCBSetSpace \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_space args) | GenInvocationLabel TCBSuspend \<Rightarrow> Some (TcbIntent TcbSuspendIntent) | GenInvocationLabel TCBResume \<Rightarrow> Some (TcbIntent TcbResumeIntent) | GenInvocationLabel TCBBindNotification \<Rightarrow> Some (TcbIntent TcbBindNTFNIntent) | GenInvocationLabel TCBUnbindNotification \<Rightarrow> Some (TcbIntent TcbUnbindNTFNIntent) | GenInvocationLabel TCBSetTLSBase \<Rightarrow> Some (TcbIntent TcbSetTLSBaseIntent) | GenInvocationLabel CNodeRevoke \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args) | GenInvocationLabel CNodeDelete \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args) | GenInvocationLabel CNodeCancelBadgedSends \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args) | GenInvocationLabel CNodeCopy \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_copy args) | GenInvocationLabel CNodeMint \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mint args) | GenInvocationLabel CNodeMove \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_move args) | GenInvocationLabel CNodeMutate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mutate args) | GenInvocationLabel CNodeRotate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_rotate args) | GenInvocationLabel CNodeSaveCaller \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args) | GenInvocationLabel IRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (transform_intent_issue_irq_handler args) | GenInvocationLabel IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent) | GenInvocationLabel IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | GenInvocationLabel IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent) | GenInvocationLabel DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args) | ArchInvocationLabel ARMPageTableMap \<Rightarrow> map_option PageTableIntent (transform_intent_page_table_map args) | ArchInvocationLabel ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent) | ArchInvocationLabel ARMPageMap \<Rightarrow> map_option PageIntent (transform_intent_page_map args) | ArchInvocationLabel ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent) | ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent) | ArchInvocationLabel ARMASIDControlMakePool \<Rightarrow> map_option AsidControlIntent (transform_cnode_index_and_depth AsidControlMakePoolIntent args) | ArchInvocationLabel ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent) | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (arch_transform_intent_issue_irq_handler args) | ArchInvocationLabel _ \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent))
 2. (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>x1 = CNodeRevoke \<and> \<not> length args < 2 \<or> x1 = CNodeDelete \<and> \<not> length args < 2 \<or> x1 = CNodeCancelBadgedSends \<and> \<not> length args < 2 \<or> x1 = CNodeCopy \<and> \<not> length args < 5 \<or> x1 = CNodeMint \<and> \<not> length args < 6 \<or> x1 = CNodeMove \<and> \<not> length args < 4 \<or> x1 = CNodeMutate \<and> \<not> length args < 5 \<or> x1 = CNodeRotate \<and> \<not> length args < 8 \<or> x1 = CNodeSaveCaller \<and> \<not> length args < 2; label = GenInvocationLabel x1\<rbrakk> \<Longrightarrow> \<exists>ui. Some (CNodeIntent ui) = (case x1 of InvalidInvocation \<Rightarrow> None | UntypedRetype \<Rightarrow> map_option UntypedIntent (transform_intent_untyped_retype args) | TCBReadRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_read_registers args) | TCBWriteRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_write_registers args) | TCBCopyRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_copy_registers args) | TCBConfigure \<Rightarrow> map_option TcbIntent (transform_intent_tcb_configure args) | TCBSetPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_priority args) | TCBSetMCPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_mcpriority args) | TCBSetSchedParams \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_sched_params args) | TCBSetIPCBuffer \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args) | TCBSetSpace \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_space args) | TCBSuspend \<Rightarrow> Some (TcbIntent TcbSuspendIntent) | TCBResume \<Rightarrow> Some (TcbIntent TcbResumeIntent) | TCBBindNotification \<Rightarrow> Some (TcbIntent TcbBindNTFNIntent) | TCBUnbindNotification \<Rightarrow> Some (TcbIntent TcbUnbindNTFNIntent) | TCBSetTLSBase \<Rightarrow> Some (TcbIntent TcbSetTLSBaseIntent) | CNodeRevoke \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args) | CNodeDelete \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args) | CNodeCancelBadgedSends \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args) | CNodeCopy \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_copy args) | CNodeMint \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mint args) | CNodeMove \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_move args) | CNodeMutate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mutate args) | CNodeRotate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_rotate args) | CNodeSaveCaller \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args) | IRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (transform_intent_issue_irq_handler args) | IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent) | IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent) | DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args))
 2. (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args proof (prove)
goal (10 subgoals):
 1. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeRevoke; gen_label = CNodeRevoke\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 2. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeDelete; gen_label = CNodeDelete\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 3. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeCancelBadgedSends; gen_label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 4. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeCopy; gen_label = CNodeCopy\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 5. \<And>gen_label. \<lbrakk>\<not> length args < 6; label = GenInvocationLabel CNodeMint; gen_label = CNodeMint\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d. x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d])))))
 6. \<And>gen_label. \<lbrakk>\<not> length args < 4; label = GenInvocationLabel CNodeMove; gen_label = CNodeMove\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b. x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b])))
 7. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeMutate; gen_label = CNodeMutate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 8. \<And>gen_label. \<lbrakk>\<not> length args < 8; label = GenInvocationLabel CNodeRotate; gen_label = CNodeRotate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d x22d. (x22d = [] \<longrightarrow> x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d]) \<and> (\<forall>x21e x22e. (x22e = [] \<longrightarrow> x22d = [x21e] \<longrightarrow> x22c = [x21d, x21e] \<longrightarrow> x22b = [x21c, x21d, x21e] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e]) \<and> (\<forall>x21f. x22e = [x21f] \<longrightarrow> x22d = [x21e, x21f] \<longrightarrow> x22c = [x21d, x21e, x21f] \<longrightarrow> x22b = [x21c, x21d, x21e, x21f] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e, x21f] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e, x21f] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e, x21f])))))))
 9. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeSaveCaller; gen_label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 10. (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args proof (prove)
goal (10 subgoals):
 1. (label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6) \<and> (label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5) \<and> (label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8) \<and> (label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2) \<Longrightarrow> \<nexists>ui. Some (CNodeIntent ui) = transform_intent label args
 2. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeRevoke; gen_label = CNodeRevoke\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 3. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeDelete; gen_label = CNodeDelete\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 4. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeCancelBadgedSends; gen_label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 5. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeCopy; gen_label = CNodeCopy\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 6. \<And>gen_label. \<lbrakk>\<not> length args < 6; label = GenInvocationLabel CNodeMint; gen_label = CNodeMint\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d. x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d])))))
 7. \<And>gen_label. \<lbrakk>\<not> length args < 4; label = GenInvocationLabel CNodeMove; gen_label = CNodeMove\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b. x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b])))
 8. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeMutate; gen_label = CNodeMutate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 9. \<And>gen_label. \<lbrakk>\<not> length args < 8; label = GenInvocationLabel CNodeRotate; gen_label = CNodeRotate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d x22d. (x22d = [] \<longrightarrow> x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d]) \<and> (\<forall>x21e x22e. (x22e = [] \<longrightarrow> x22d = [x21e] \<longrightarrow> x22c = [x21d, x21e] \<longrightarrow> x22b = [x21c, x21d, x21e] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e]) \<and> (\<forall>x21f. x22e = [x21f] \<longrightarrow> x22d = [x21e, x21f] \<longrightarrow> x22c = [x21d, x21e, x21f] \<longrightarrow> x22b = [x21c, x21d, x21e, x21f] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e, x21f] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e, x21f] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e, x21f])))))))
 10. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeSaveCaller; gen_label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21]) proof (prove)
goal (10 subgoals):
 1. \<And>ui. \<lbrakk>label = GenInvocationLabel CNodeRevoke \<longrightarrow> length args < 2; label = GenInvocationLabel CNodeDelete \<longrightarrow> length args < 2; label = GenInvocationLabel CNodeCancelBadgedSends \<longrightarrow> length args < 2; label = GenInvocationLabel CNodeCopy \<longrightarrow> length args < 5; label = GenInvocationLabel CNodeMint \<longrightarrow> length args < 6; label = GenInvocationLabel CNodeMove \<longrightarrow> length args < 4; label = GenInvocationLabel CNodeMutate \<longrightarrow> length args < 5; label = GenInvocationLabel CNodeRotate \<longrightarrow> length args < 8; label = GenInvocationLabel CNodeSaveCaller \<longrightarrow> length args < 2; Some (CNodeIntent ui) = transform_intent label args\<rbrakk> \<Longrightarrow> False
 2. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeRevoke; gen_label = CNodeRevoke\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 3. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeDelete; gen_label = CNodeDelete\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 4. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeCancelBadgedSends; gen_label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 5. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeCopy; gen_label = CNodeCopy\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 6. \<And>gen_label. \<lbrakk>\<not> length args < 6; label = GenInvocationLabel CNodeMint; gen_label = CNodeMint\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d. x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d])))))
 7. \<And>gen_label. \<lbrakk>\<not> length args < 4; label = GenInvocationLabel CNodeMove; gen_label = CNodeMove\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b. x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b])))
 8. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeMutate; gen_label = CNodeMutate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 9. \<And>gen_label. \<lbrakk>\<not> length args < 8; label = GenInvocationLabel CNodeRotate; gen_label = CNodeRotate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d x22d. (x22d = [] \<longrightarrow> x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d]) \<and> (\<forall>x21e x22e. (x22e = [] \<longrightarrow> x22d = [x21e] \<longrightarrow> x22c = [x21d, x21e] \<longrightarrow> x22b = [x21c, x21d, x21e] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e]) \<and> (\<forall>x21f. x22e = [x21f] \<longrightarrow> x22d = [x21e, x21f] \<longrightarrow> x22c = [x21d, x21e, x21f] \<longrightarrow> x22b = [x21c, x21d, x21e, x21f] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e, x21f] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e, x21f] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e, x21f])))))))
 10. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeSaveCaller; gen_label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21]) proof (prove)
goal (9 subgoals):
 1. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeRevoke; gen_label = CNodeRevoke\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 2. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeDelete; gen_label = CNodeDelete\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 3. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeCancelBadgedSends; gen_label = CNodeCancelBadgedSends\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21])
 4. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeCopy; gen_label = CNodeCopy\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 5. \<And>gen_label. \<lbrakk>\<not> length args < 6; label = GenInvocationLabel CNodeMint; gen_label = CNodeMint\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d. x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d])))))
 6. \<And>gen_label. \<lbrakk>\<not> length args < 4; label = GenInvocationLabel CNodeMove; gen_label = CNodeMove\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b. x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b])))
 7. \<And>gen_label. \<lbrakk>\<not> length args < 5; label = GenInvocationLabel CNodeMutate; gen_label = CNodeMutate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c. x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]))))
 8. \<And>gen_label. \<lbrakk>\<not> length args < 8; label = GenInvocationLabel CNodeRotate; gen_label = CNodeRotate\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21 x22. (x22 = [] \<longrightarrow> args \<noteq> [x21]) \<and> (\<forall>x21a x22a. (x22a = [] \<longrightarrow> x22 = [x21a] \<longrightarrow> args \<noteq> [x21, x21a]) \<and> (\<forall>x21b x22b. (x22b = [] \<longrightarrow> x22a = [x21b] \<longrightarrow> x22 = [x21a, x21b] \<longrightarrow> args \<noteq> [x21, x21a, x21b]) \<and> (\<forall>x21c x22c. (x22c = [] \<longrightarrow> x22b = [x21c] \<longrightarrow> x22a = [x21b, x21c] \<longrightarrow> x22 = [x21a, x21b, x21c] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c]) \<and> (\<forall>x21d x22d. (x22d = [] \<longrightarrow> x22c = [x21d] \<longrightarrow> x22b = [x21c, x21d] \<longrightarrow> x22a = [x21b, x21c, x21d] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d]) \<and> (\<forall>x21e x22e. (x22e = [] \<longrightarrow> x22d = [x21e] \<longrightarrow> x22c = [x21d, x21e] \<longrightarrow> x22b = [x21c, x21d, x21e] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e]) \<and> (\<forall>x21f. x22e = [x21f] \<longrightarrow> x22d = [x21e, x21f] \<longrightarrow> x22c = [x21d, x21e, x21f] \<longrightarrow> x22b = [x21c, x21d, x21e, x21f] \<longrightarrow> x22a = [x21b, x21c, x21d, x21e, x21f] \<longrightarrow> x22 = [x21a, x21b, x21c, x21d, x21e, x21f] \<longrightarrow> args \<noteq> [x21, x21a, x21b, x21c, x21d, x21e, x21f])))))))
 9. \<And>gen_label. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel CNodeSaveCaller; gen_label = CNodeSaveCaller\<rbrakk> \<Longrightarrow> args \<noteq> [] \<and> (\<forall>x21. args \<noteq> [x21]) proof (prove)
goal:
No subgoals!