theory Invoke_C

lemma fromEnum_object_type_to_H:
  "fromEnum x = unat (object_type_from_H x)" apply (cut_tac eqset_imp_iff[where x=x, OF enum_surj]) apply (simp add: fromEnum_def enum_object_type
                   enum_apiobject_type
                   object_type_from_H_def
                   "StrictC'_object_defs" "api_object_defs"
            split: if_split) apply (auto simp: "api_object_defs") done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum x = unat (object_type_from_H x) proof (prove)
goal (1 subgoal):
 1. (x \<in> set enum) = (x \<in> UNIV) \<Longrightarrow> fromEnum x = unat (object_type_from_H x) proof (prove)
goal (1 subgoal):
 1. x = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> x = APIObjectType ArchTypes_H.apiobject_type.TCBObject \<or> x = APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<or> x = APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<or> x = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<or> x = object_type.PageDirectoryObject \<or> x = object_type.SmallPageObject \<or> x = object_type.LargePageObject \<or> x = object_type.SectionObject \<or> x = object_type.SuperSectionObject \<or> x = object_type.PageTableObject \<Longrightarrow> object_type.PageTableObject \<noteq> x \<longrightarrow> object_type.SuperSectionObject \<noteq> x \<longrightarrow> object_type.SectionObject \<noteq> x \<longrightarrow> object_type.LargePageObject \<noteq> x \<longrightarrow> object_type.SmallPageObject \<noteq> x \<longrightarrow> object_type.PageDirectoryObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.CapTableObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.NotificationObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc 0) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject)))) \<and> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc (Suc 0)) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))))) \<and> (APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc 0) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject)))) \<and> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc (Suc (Suc 0))) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject)))))) \<and> (APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.NotificationObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc 0) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject)))) \<and> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc (Suc 0)) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))))) \<and> (APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc 0) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject)))) \<and> (APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.TCBObject = x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc 0 = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject))) \<and> (APIObjectType ArchTypes_H.apiobject_type.TCBObject \<noteq> x \<longrightarrow> (APIObjectType ArchTypes_H.apiobject_type.Untyped = x \<longrightarrow> unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = 0) \<and> (APIObjectType ArchTypes_H.apiobject_type.Untyped \<noteq> x \<longrightarrow> Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the_index [] x))))))))))) = unat (case x of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject | object_type.SmallPageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject | object_type.LargePageObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject | object_type.SectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject | object_type.SuperSectionObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject | object_type.PageTableObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject | object_type.PageDirectoryObject \<Rightarrow> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject)))))) proof (prove)
goal:
No subgoals!