:: AMISTD_4 semantic presentation begin definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "A")); let "o" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Const "o"))); :: original: :::"+*"::: redefine func "s" :::"+*"::: "(" "o" "," "a" ")" -> ($#m1_hidden :::"State":::) "of" "A"; end; theorem :: AMISTD_4:1 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "st" (Bool (Bool (Set (Var "I")) "is" ($#v4_amistd_1 :::"sequential"::: ) ) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"IC"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "s")) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "w")) ")" ")" ) ")" ")" ))))))))) ; theorem :: AMISTD_4:2 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "st" (Bool (Bool (Set (Var "I")) "is" ($#v4_amistd_1 :::"sequential"::: ) ) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"IC"::: ) ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "s")) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "w")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "w")) ")" ")" ))))))))) ; begin definitionlet "A" be ($#l1_compos_1 :::"COM-Struct"::: ) ; attr "A" is :::"with_non_trivial_Instructions"::: means :: AMISTD_4:def 1 (Bool (Bool "not" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "A") "is" ($#v1_zfmisc_1 :::"trivial"::: ) )); end; :: deftheorem defines :::"with_non_trivial_Instructions"::: AMISTD_4:def 1 : (Bool "for" (Set (Var "A")) "being" ($#l1_compos_1 :::"COM-Struct"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ) "iff" (Bool (Bool "not" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "A"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) ")" )); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); attr "A" is :::"with_non_trivial_ObjectKinds"::: means :: AMISTD_4:def 2 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Bool "not" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))); end; :: deftheorem defines :::"with_non_trivial_ObjectKinds"::: AMISTD_4:def 2 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Bool "not" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_amistd_1 :::"STC"::: ) "N") -> ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#v2_amistd_2 :::"with_explicit_jumps"::: ) ($#v4_amistd_2 :::"IC-relocable"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_amistd_1 :::"STC"::: ) "N") -> ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "o" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")); cluster (Set ($#k4_memstr_0 :::"Values"::: ) "o") -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); cluster (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "A") -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); cluster (Set ($#k4_memstr_0 :::"Values"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "I" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "A")); func :::"Output"::: "I" -> ($#m1_subset_1 :::"Subset":::) "of" "A" means :: AMISTD_4:def 3 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "A" "st" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" "I" "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) ")" )); end; :: deftheorem defines :::"Output"::: AMISTD_4:def 3 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))))) ")" )) ")" ))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "I" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "A")); func :::"Out_\_Inp"::: "I" -> ($#m1_subset_1 :::"Subset":::) "of" "A" means :: AMISTD_4:def 4 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "A" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" "I" "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" "I" "," (Set "(" (Set (Var "s")) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" ")" ) ")" )))) ")" )); func :::"Out_U_Inp"::: "I" -> ($#m1_subset_1 :::"Subset":::) "of" "A" means :: AMISTD_4:def 5 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "A"(Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "st" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" "I" "," (Set "(" (Set (Var "s")) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" "I" "," (Set (Var "s")) ")" ")" ) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" )))) ")" )); end; :: deftheorem defines :::"Out_\_Inp"::: AMISTD_4:def 4 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_amistd_4 :::"Out_\_Inp"::: ) (Set (Var "I")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "s")) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" ")" ) ")" )))) ")" )) ")" ))))); :: deftheorem defines :::"Out_U_Inp"::: AMISTD_4:def 5 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "st" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "s")) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_amistd_4 :::"+*"::: ) "(" (Set (Var "o")) "," (Set (Var "a")) ")" )))) ")" )) ")" ))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "I" be ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "A")); func :::"Input"::: "I" -> ($#m1_subset_1 :::"Subset":::) "of" "A" equals :: AMISTD_4:def 6 (Set (Set "(" ($#k4_amistd_4 :::"Out_U_Inp"::: ) "I" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_amistd_4 :::"Out_\_Inp"::: ) "I" ")" )); end; :: deftheorem defines :::"Input"::: AMISTD_4:def 6 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k5_amistd_4 :::"Input"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_amistd_4 :::"Out_\_Inp"::: ) (Set (Var "I")) ")" )))))); theorem :: AMISTD_4:3 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k3_amistd_4 :::"Out_\_Inp"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))))))) ; theorem :: AMISTD_4:4 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I"))))))) ; theorem :: AMISTD_4:5 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k3_amistd_4 :::"Out_\_Inp"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k5_amistd_4 :::"Input"::: ) (Set (Var "I")) ")" )))))) ; theorem :: AMISTD_4:6 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k5_amistd_4 :::"Input"::: ) (Set (Var "I")) ")" )))))) ; theorem :: AMISTD_4:7 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) "holds" (Bool "not" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I"))))))))) ; theorem :: AMISTD_4:8 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) "holds" (Bool "not" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k5_amistd_4 :::"Input"::: ) (Set (Var "I"))))))))) ; theorem :: AMISTD_4:9 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "o"))) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )) "holds" (Bool "not" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))))))))) ; theorem :: AMISTD_4:10 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ) "iff" (Bool (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )))) ; theorem :: AMISTD_4:11 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set ($#k3_amistd_4 :::"Out_\_Inp"::: ) (Set (Var "I"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: AMISTD_4:12 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: AMISTD_4:13 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set ($#k5_amistd_4 :::"Input"::: ) (Set (Var "I"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "I" be ($#v2_extpro_1 :::"halting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "A")); cluster (Set ($#k5_amistd_4 :::"Input"::: ) "I") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k2_amistd_4 :::"Output"::: ) "I") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) "I") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#v2_amistd_4 :::"with_non_trivial_ObjectKinds"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "I" be ($#v2_extpro_1 :::"halting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "A")); cluster (Set ($#k3_amistd_4 :::"Out_\_Inp"::: ) "I") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_amistd_4 :::"with_non_trivial_Instructions"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; theorem :: AMISTD_4:14 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v4_amistd_1 :::"sequential"::: ) )) "holds" (Bool "not" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_amistd_4 :::"Out_\_Inp"::: ) (Set (Var "I")))))))) ; theorem :: AMISTD_4:15 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) "st" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")))))) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_amistd_1 :::"standard"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; theorem :: AMISTD_4:16 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v4_amistd_1 :::"sequential"::: ) )) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))))))) ; theorem :: AMISTD_4:17 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "A")) "st" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")))))) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I"))))))) ; theorem :: AMISTD_4:18 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v4_amistd_1 :::"sequential"::: ) )) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_amistd_4 :::"Out_U_Inp"::: ) (Set (Var "I"))))))) ; theorem :: AMISTD_4:19 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_amistd_1 :::"jump-only"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set ($#k2_amistd_4 :::"Output"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"IC"::: ) )))))) ;