:: AMISTD_2  semantic presentation begin  




















theorem :: AMISTD_2:1 (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")) ")" ) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 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"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); let "I" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); attr "I" is  :::"with_explicit_jumps":::  means :: AMISTD_2:def 1 (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  "I")  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k5_xtuple_0 :::"JumpPart"::: )  "I" ")" ))); end; 






:: deftheorem    defines :::"with_explicit_jumps"::: AMISTD_2: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"::: )     ($#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_2 :::"with_explicit_jumps"::: )  ) "iff" (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k5_xtuple_0 :::"JumpPart"::: )  (Set (Var "I")) ")" )))  ")" )))); 
 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"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); attr "S" is  :::"with_explicit_jumps":::  means :: AMISTD_2:def 2 (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" "S" "holds"  (Bool (Set (Var "I")) "is"   ($#v1_amistd_2 :::"with_explicit_jumps"::: )  )); end; 





:: deftheorem    defines :::"with_explicit_jumps"::: AMISTD_2: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"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_amistd_2 :::"with_explicit_jumps"::: )  ) "iff" (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "I")) "is"   ($#v1_amistd_2 :::"with_explicit_jumps"::: )  ))  ")" ))); 
 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_2: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_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 "S"))  "st" (Bool (Bool  "("   "for" (Set (Var "f")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set (Var "I")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "f")) ")" ) ($#k1_tarski :::"}"::: ) ))  ")" )) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set (Var "I"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 registrationlet "N" be   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )  ; let "I" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  "("  ($#k4_amistd_1 :::"STC"::: )  (Set (Const "N")) ")" ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  "I") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: AMISTD_2:3 (Bool  "for" (Set (Var "N")) "being"   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k4_amistd_1 :::"STC"::: )  (Set (Var "N")) ")" )) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 registrationlet "N" be   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_amistd_1 :::"STC"::: )  "N") ->   ($#v2_amistd_2 :::"with_explicit_jumps"::: )   ; 
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_2 :::"with_explicit_jumps"::: )    for    ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" "N"; 
end; registrationlet "N" be   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )  ; let "I" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  "("  ($#k1_extpro_1 :::"Trivial-AMI"::: )  (Set (Const "N")) ")" ); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  "I") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "N" be   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_extpro_1 :::"Trivial-AMI"::: )  "N") ->   ($#v2_amistd_2 :::"with_explicit_jumps"::: )   ; 
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"::: )    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"::: )     ($#v2_amistd_2 :::"with_explicit_jumps"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster   ->   ($#v1_amistd_2 :::"with_explicit_jumps"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
end; 
theorem :: AMISTD_2: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"::: )     ($#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_extpro_1 :::"halting"::: )  )) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set (Var "I"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 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")); let "I" be   ($#v2_extpro_1 :::"halting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  "I") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: AMISTD_2: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_2 :::"with_explicit_jumps"::: )     ($#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"   ($#v4_compos_0 :::"ins-loc-free"::: )  )) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set (Var "I"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 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"::: )     ($#v2_amistd_2 :::"with_explicit_jumps"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster   ($#v2_extpro_1 :::"halting"::: )    ->   ($#v4_compos_0 :::"ins-loc-free"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
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"::: )     ($#v2_amistd_2 :::"with_explicit_jumps"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster   ($#v4_amistd_1 :::"sequential"::: )    ->   ($#v4_compos_0 :::"ins-loc-free"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster (Set   ($#k4_compos_1 :::"Stop"::: )  "S") ->   ($#v5_amistd_1 :::"really-closed"::: )   ; 
end; begin  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   ($#v2_extpro_1 :::"halting"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set (Const "S")); let "k" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" "I" "," "k" ")" ) ->   ($#v2_extpro_1 :::"halting"::: )   ; 
end; 
theorem :: AMISTD_2:6 (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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#v2_amistd_2 :::"with_explicit_jumps"::: )     ($#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"   ($#v4_amistd_1 :::"sequential"::: )  )) "holds"  (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "I")) "," (Set (Var "k")) ")" ) "is"   ($#v4_amistd_1 :::"sequential"::: )  ))))) ; 
 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  :::"IC-relocable":::  means :: AMISTD_2:def 3 (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 (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "("  ($#k5_compos_0 :::"IncAddr"::: )   "(" "I" "," (Set (Var "j")) ")"  ")" ) "," (Set (Var "s")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (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")) ")"  ")" ) ")"  ")" ))))); end; 






:: deftheorem    defines :::"IC-relocable"::: AMISTD_2: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"))  (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "I")) "is"   ($#v3_amistd_2 :::"IC-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 (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "("  ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "I")) "," (Set (Var "j")) ")"  ")" ) "," (Set (Var "s")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (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")) ")"  ")" ) ")"  ")" )))))  ")" )))); 
 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-relocable":::  means :: AMISTD_2:def 4 (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" "S" "holds"  (Bool (Set (Var "I")) "is"   ($#v3_amistd_2 :::"IC-relocable"::: )  )); end; 





:: deftheorem    defines :::"IC-relocable"::: AMISTD_2: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_2 :::"IC-relocable"::: )  ) "iff" (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "I")) "is"   ($#v3_amistd_2 :::"IC-relocable"::: )  ))  ")" ))); 
 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")); 
cluster   ($#v4_amistd_1 :::"sequential"::: )    ->   ($#v3_amistd_2 :::"IC-relocable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
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_2 :::"with_explicit_jumps"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster   ($#v2_extpro_1 :::"halting"::: )    ->   ($#v3_amistd_2 :::"IC-relocable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
end; registrationlet "N" be   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_amistd_1 :::"STC"::: )  "N") ->   ($#v4_amistd_2 :::"IC-relocable"::: )   ; 
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_2 :::"with_explicit_jumps"::: )    for    ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" "N"; 
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_2 :::"with_explicit_jumps"::: )     ($#v4_amistd_2 :::"IC-relocable"::: )    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"::: )     ($#v4_amistd_2 :::"IC-relocable"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster   ->   ($#v3_amistd_2 :::"IC-relocable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
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_2 :::"with_explicit_jumps"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); 
cluster   ($#v1_amistd_2 :::"with_explicit_jumps"::: )     ($#v3_amistd_2 :::"IC-relocable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" "S"); 
end; 
theorem :: AMISTD_2: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"::: )     ($#v2_amistd_2 :::"with_explicit_jumps"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N"))  (Bool  "for" (Set (Var "I")) "being"   ($#v3_amistd_2 :::"IC-relocable"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "I")) "," (Set (Var "s")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "("  ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "I")) "," (Set (Var "k")) ")"  ")" ) "," (Set  "("  ($#k9_memstr_0 :::"IncIC"::: )   "(" (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"::: )     ($#v3_amistd_1 :::"standard"::: )     ($#v2_amistd_2 :::"with_explicit_jumps"::: )     ($#v4_amistd_2 :::"IC-relocable"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Const "N")); let "F", "G" be (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set (Const "S")))  ($#v5_relat_1 :::"-valued"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )     ($#v5_amistd_1 :::"really-closed"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "F"  ($#k7_compos_1 :::"';'"::: )  "G") ->   ($#v5_amistd_1 :::"really-closed"::: )   ; 
end; 
theorem :: AMISTD_2:8 (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  "("  ($#k1_extpro_1 :::"Trivial-AMI"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set   ($#k5_xtuple_0 :::"JumpPart"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: AMISTD_2:9 (Bool  "for" (Set (Var "N")) "being"   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"InsType":::) "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  "("  ($#k1_extpro_1 :::"Trivial-AMI"::: )  (Set (Var "N")) ")" )) "holds"  (Bool (Set   ($#k3_compos_0 :::"JumpParts"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 




theorem :: AMISTD_2:10 (Bool  "for" (Set (Var "N")) "being"   ($#v1_setfam_1 :::"with_zero"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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 "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "I"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "I"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2"))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "m")) ")"  ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "I"))))  ")" )) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s")) "," (Set (Var "m")) ")" )  ($#r8_pboole :::"="::: )  (Set   ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ))))))))) ; 
 
theorem :: AMISTD_2: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"::: )     ($#l1_extpro_1 :::"AMI-Struct"::: )   "over" (Set (Var "N"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "s"))  ($#r8_pboole :::"="::: )  (Set   ($#k4_extpro_1 :::"Following"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) ")" ))) "holds"  (Bool  "for" (Set (Var "n")) "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 "n")) ")" )  ($#r8_pboole :::"="::: )  (Set (Var "s")))))))) ;