:: AMISTD_5 semantic presentation begin theorem :: AMISTD_5:1 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "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 "S")) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_amistd_1 :::"jump-only"::: ) )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ) "is" ($#v2_amistd_1 :::"jump-only"::: ) ))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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_2 :::"with_explicit_jumps"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "I" be ($#v3_amistd_2 :::"IC-relocable"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" "I" "," "k" ")" ) -> ($#v3_amistd_2 :::"IC-relocable"::: ) ; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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 ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); attr "I" is :::"relocable"::: means :: AMISTD_5:def 1 (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "S" "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" "I" "," (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" ) "," (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" "I" "," (Set (Var "j")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "k")) ")" )))); end; :: deftheorem defines :::"relocable"::: AMISTD_5:def 1 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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 (Var "N")) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_amistd_5 :::"relocable"::: ) ) "iff" (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" ) "," (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "I")) "," (Set (Var "j")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "k")) ")" )))) ")" )))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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")); cluster ($#v1_amistd_5 :::"relocable"::: ) -> ($#v3_amistd_2 :::"IC-relocable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S"); end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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")); attr "S" is :::"relocable"::: means :: AMISTD_5:def 2 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" "S" "holds" (Bool (Set (Var "I")) "is" ($#v1_amistd_5 :::"relocable"::: ) )); end; :: deftheorem defines :::"relocable"::: AMISTD_5:def 2 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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 (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_amistd_5 :::"relocable"::: ) ) "iff" (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "I")) "is" ($#v1_amistd_5 :::"relocable"::: ) )) ")" ))); theorem :: AMISTD_5:2 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k4_amistd_1 :::"STC"::: ) (Set (Var "N")) ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k4_amistd_1 :::"STC"::: ) (Set (Var "N")) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "k")) ")" )))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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")); attr "S" is :::"IC-recognized"::: means :: AMISTD_5:def 3 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" "S" "st" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))))); end; :: deftheorem defines :::"IC-recognized"::: AMISTD_5:def 3 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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 (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_amistd_5 :::"IC-recognized"::: ) ) "iff" (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))))) ")" ))); theorem :: AMISTD_5:3 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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 (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_amistd_5 :::"IC-recognized"::: ) ) "iff" (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))))) ")" ))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_struct_0 :::"NonZero"::: ) (Set "(" ($#k4_amistd_1 :::"STC"::: ) "N" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"PartState":::) "of" (Set "(" ($#k4_amistd_1 :::"STC"::: ) (Set (Const "N")) ")" ); cluster (Set ($#k6_memstr_0 :::"DataPart"::: ) "p") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_amistd_1 :::"STC"::: ) "N") -> ($#v2_amistd_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ; 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"::: ) ($#v3_amistd_1 :::"standard"::: ) ($#v2_amistd_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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_5 :::"relocable"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); cluster -> ($#v1_amistd_5 :::"relocable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S"); end; theorem :: AMISTD_5:4 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "INS")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "INS")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "INS")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "k")) ")" ))))))) ; theorem :: AMISTD_5:5 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "INS")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "INS")) "," (Set "(" ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "INS")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "k")) ")" ))))))) ; 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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; theorem :: AMISTD_5:6 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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")); attr "S" is :::"CurIns-recognized"::: means :: AMISTD_5:def 4 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" "S" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))))))); end; :: deftheorem defines :::"CurIns-recognized"::: AMISTD_5:def 4 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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 (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_amistd_5 :::"CurIns-recognized"::: ) ) "iff" (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))))))) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_amistd_1 :::"STC"::: ) "N") -> ($#v4_amistd_5 :::"CurIns-recognized"::: ) ; 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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; theorem :: AMISTD_5:7 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) ")" )))))))) ; theorem :: AMISTD_5:8 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b4")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set (Var "i")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "k")) ")" )))))))))) ; theorem :: AMISTD_5:9 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b4")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "k")) ")" )))))))))) ; theorem :: AMISTD_5:10 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) "is" (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#v4_extpro_1 :::"-autonomic"::: ) )) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k10_memstr_0 :::"DecIC"::: ) "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "k")) ")" )))))))))) ; theorem :: AMISTD_5:11 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" (Set (Var "q")) ($#v4_extpro_1 :::"-autonomic"::: ) ) "iff" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) "is" (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#v4_extpro_1 :::"-autonomic"::: ) ) ")" )))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); attr "S" is :::"relocable1"::: means :: AMISTD_5:def 5 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b2")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" "S" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )))))))); attr "S" is :::"relocable2"::: means :: AMISTD_5:def 6 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b2")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" "S" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" ))))))))); end; :: deftheorem defines :::"relocable1"::: AMISTD_5:def 5 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_amistd_5 :::"relocable1"::: ) ) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b4")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )))))))) ")" ))); :: deftheorem defines :::"relocable2"::: AMISTD_5:def 6 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_amistd_5 :::"relocable2"::: ) ) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b4")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "p")) ")" ) ")" ))))))))) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_amistd_1 :::"STC"::: ) "N") -> ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) ; 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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; theorem :: AMISTD_5:12 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Var "p")) "is" (Set (Var "q")) ($#v5_extpro_1 :::"-halted"::: ) ) "iff" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) "is" (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) ($#v5_extpro_1 :::"-halted"::: ) ) ")" )))))) ; theorem :: AMISTD_5:13 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) (Set (Var "b3")) ($#v5_extpro_1 :::"-halted"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k7_extpro_1 :::"Result"::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k7_extpro_1 :::"Result"::: ) "(" (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ) ")" ")" )))))))) ; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "q" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); let "p" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Const "q")) ($#v4_extpro_1 :::"-autonomic"::: ) (Set (Const "q")) ($#v5_extpro_1 :::"-halted"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" "p" "," "k" ")" ) -> (Set ($#k6_compos_1 :::"Reloc"::: ) "(" "q" "," "k" ")" ) ($#v5_extpro_1 :::"-halted"::: ) ; end; theorem :: AMISTD_5:14 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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_5 :::"relocable"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#v5_amistd_5 :::"relocable1"::: ) ($#v6_amistd_5 :::"relocable2"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "F")) "being" ($#v6_memstr_0 :::"data-only"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k11_memstr_0 :::"FinPartSt"::: ) (Set (Var "S")) ")" ) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b5")) ($#v4_extpro_1 :::"-autonomic"::: ) (Set (Var "b5")) ($#v5_extpro_1 :::"-halted"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) "," (Set (Var "p")) ($#r2_extpro_1 :::"computes"::: ) (Set (Var "F"))) "iff" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "q")) "," (Set (Var "k")) ")" ) "," (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r2_extpro_1 :::"computes"::: ) (Set (Var "F"))) ")" )))))))) ; theorem :: AMISTD_5:15 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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"::: ) ($#v3_amistd_5 :::"IC-recognized"::: ) ($#v4_amistd_5 :::"CurIns-recognized"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")))))))) ; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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 "k" be ($#m1_hidden :::"Nat":::); let "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); attr "F" is "k" :::"-halting"::: means :: AMISTD_5:def 7 (Bool "for" (Set (Var "s")) "being" "k" ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" "S" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool "F" ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))); end; :: deftheorem defines :::"-halting"::: AMISTD_5:def 7 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~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 (Var "N")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Var "k")) ($#v7_amistd_5 :::"-halting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))) ")" ))))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" 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")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v7_amistd_1 :::"parahalting"::: ) -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v7_amistd_5 :::"-halting"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#v7_amistd_5 :::"-halting"::: ) -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S") ($#v5_relat_1 :::"-valued"::: ) ($#v7_amistd_1 :::"parahalting"::: ) for ($#m1_hidden :::"set"::: ) ; end;