:: EXTPRO_1 semantic presentation begin definitionlet "N" be ($#m1_hidden :::"set"::: ) ; attr "c2" is :::"strict"::: ; struct :::"AMI-Struct"::: "over" "N" -> ($#l1_memstr_0 :::"Mem-Struct"::: ) "over" "N" "," ($#l1_compos_1 :::"COM-Struct"::: ) ; aggr :::"AMI-Struct":::(# :::"carrier":::, :::"ZeroF":::, :::"InstructionsF":::, :::"Object-Kind":::, :::"ValuesF":::, :::"Execution"::: #) -> ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; sel :::"Execution"::: "c2" -> ($#m1_subset_1 :::"Action":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "c2") "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" "c2") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" "c2") ")" ) ")" ); end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Trivial-AMI"::: "N" -> ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N" means :: EXTPRO_1:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "N" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Set "the" ($#u1_extpro_1 :::"Execution"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" "N" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ))) ")" ); end; :: deftheorem defines :::"Trivial-AMI"::: EXTPRO_1:def 1 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_extpro_1 :::"Trivial-AMI"::: ) (Set (Var "N")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_memstr_0 :::"Object-Kind"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set "the" ($#u2_memstr_0 :::"ValuesF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Set "the" ($#u1_extpro_1 :::"Execution"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set "(" (Set (Var "N")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_extpro_1 :::"Trivial-AMI"::: ) "N") -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_extpro_1 :::"Trivial-AMI"::: ) "N") -> ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#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 "S")); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); func :::"Exec"::: "(" "I" "," "s" ")" -> ($#m1_hidden :::"State":::) "of" "S" equals :: EXTPRO_1:def 2 (Set (Set "(" (Set "the" ($#u1_extpro_1 :::"Execution"::: ) "of" "S") ($#k3_funct_2 :::"."::: ) "I" ")" ) ($#k1_funct_1 :::"."::: ) "s"); end; :: deftheorem defines :::"Exec"::: EXTPRO_1:def 2 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#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 "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_extpro_1 :::"Execution"::: ) "of" (Set (Var "S"))) ($#k3_funct_2 :::"."::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))))))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#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 "S")); attr "I" is :::"halting"::: means :: EXTPRO_1:def 3 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "S" "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" "I" "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s")))); end; :: deftheorem defines :::"halting"::: EXTPRO_1:def 3 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#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 "S")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s")))) ")" )))); definitionlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); attr "S" is :::"halting"::: means :: EXTPRO_1:def 4 (Bool (Set ($#k2_compos_1 :::"halt"::: ) "S") "is" ($#v2_extpro_1 :::"halting"::: ) ); end; :: deftheorem defines :::"halting"::: EXTPRO_1:def 4 : (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_extpro_1 :::"halting"::: ) ) "iff" (Bool (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))) "is" ($#v2_extpro_1 :::"halting"::: ) ) ")" ))); registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_extpro_1 :::"Trivial-AMI"::: ) "N") -> ($#v1_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) ; 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_extpro_1 :::"halting"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); cluster (Set ($#k2_compos_1 :::"halt"::: ) "S") -> ($#v2_extpro_1 :::"halting"::: ) ; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); cluster ($#v2_extpro_1 :::"halting"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" "S"); end; theorem :: EXTPRO_1:1 (Bool "for" (Set (Var "N")) "being" ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set "(" ($#k1_extpro_1 :::"Trivial-AMI"::: ) (Set (Var "N")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set "(" ($#k1_extpro_1 :::"Trivial-AMI"::: ) (Set (Var "N")) ")" ) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s")))))) ; registrationlet "E" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_extpro_1 :::"Trivial-AMI"::: ) "E") -> ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registrationlet "M" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "M"; end; registrationlet "N" be ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; begin 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 "p" be (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); func :::"CurInstr"::: "(" "p" "," "s" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" "S" equals :: EXTPRO_1:def 5 (Set "p" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) "s" ")" )); end; :: deftheorem defines :::"CurInstr"::: EXTPRO_1: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"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))))))); 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 "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); let "p" be (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func :::"Following"::: "(" "p" "," "s" ")" -> ($#m1_hidden :::"State":::) "of" "S" equals :: EXTPRO_1:def 6 (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" "p" "," "s" ")" ")" ) "," "s" ")" ); end; :: deftheorem defines :::"Following"::: EXTPRO_1: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"::: ) ($#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 "p")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_extpro_1 :::"Following"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "s")) ")" )))))); 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 "p" 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":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); let "k" be ($#m1_hidden :::"Nat":::); func :::"Comput"::: "(" "p" "," "s" "," "k" ")" -> ($#m1_hidden :::"State":::) "of" "S" means :: EXTPRO_1:def 7 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) "S" ")" ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) "k")) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "s") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_extpro_1 :::"Following"::: ) "(" "p" "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Comput"::: EXTPRO_1: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"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set (Var "S")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_extpro_1 :::"Following"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (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"::: ) ($#v3_extpro_1 :::"halting"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Const "N")); let "p" 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":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); pred "p" :::"halts_on"::: "s" means :: EXTPRO_1:def 8 (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" "p" "," "s" "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" "p" "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" "p" "," "s" "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")) ")" )); end; :: deftheorem defines :::"halts_on"::: EXTPRO_1:def 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"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Set (Var "N")) (Bool "for" (Set (Var "p")) "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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) ")" )) ")" ))))); registrationlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" 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":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); reduce ; end; theorem :: EXTPRO_1:2 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p")) "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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))))))) ; theorem :: EXTPRO_1:3 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p")) "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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_extpro_1 :::"Following"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ))))))) ; theorem :: EXTPRO_1:4 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b3"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "k")) ")" )))))))) ; theorem :: EXTPRO_1:5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b4"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ))))))) ; definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" 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":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); assume (Bool (Set (Const "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Const "s"))) ; func :::"Result"::: "(" "p" "," "s" ")" -> ($#m1_hidden :::"State":::) "of" "S" means :: EXTPRO_1:def 9 (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" "p" "," "s" "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" "p" "," it ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")) ")" )); end; :: deftheorem defines :::"Result"::: EXTPRO_1:def 9 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" )) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set (Var "b5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) ")" )) ")" )))))); theorem :: EXTPRO_1:6 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ))))))) ; theorem :: EXTPRO_1:7 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))))) ; theorem :: EXTPRO_1:8 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ")" ))))))) ; definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" 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":::); let "IT" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); attr "IT" is "p" :::"-autonomic"::: means :: EXTPRO_1:def 10 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool "p" ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool "p" ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "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 "P")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "IT" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "IT" ")" )))))); end; :: deftheorem defines :::"-autonomic"::: EXTPRO_1:def 10 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p")) "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":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" (Set (Var "p")) ($#v4_extpro_1 :::"-autonomic"::: ) ) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "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 "P")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT")) ")" )))))) ")" ))))); definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" 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":::); let "IT" be ($#m1_hidden :::"PartState":::) "of" (Set (Const "S")); attr "IT" is "p" :::"-halted"::: means :: EXTPRO_1:def 11 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool "p" ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))); end; :: deftheorem defines :::"-halted"::: EXTPRO_1:def 11 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" (Set (Var "p")) ($#v5_extpro_1 :::"-halted"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "IT")) ($#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 "p")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))) ")" ))))); registrationlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; begin theorem :: EXTPRO_1:9 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "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":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "l"))) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "I"))))))))) ; theorem :: EXTPRO_1:10 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "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":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "p")) "is" (Set (Var "P")) ($#v5_extpro_1 :::"-halted"::: ) )))))) ; theorem :: EXTPRO_1:11 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "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":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "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 "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")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s")))))))))) ; theorem :: EXTPRO_1:12 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "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":::) "st" (Bool (Bool (Set (Set (Var "l")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "p")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"PartState":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "p")) "is" (Set (Var "P")) ($#v4_extpro_1 :::"-autonomic"::: ) )))))) ; registrationlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "P" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) "S") ($#v5_funct_1 :::"-compatible"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) bbbadV2_PRE_POLY() "P" ($#v4_extpro_1 :::"-autonomic"::: ) "P" ($#v5_extpro_1 :::"-halted"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "P" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); mode :::"Autonomy"::: "of" "P" -> ($#m1_hidden :::"FinPartState":::) "of" "S" means :: EXTPRO_1:def 12 (Bool "(" (Bool it "is" "P" ($#v4_extpro_1 :::"-autonomic"::: ) ) & (Bool it "is" "P" ($#v5_extpro_1 :::"-halted"::: ) ) ")" ); end; :: deftheorem defines :::"Autonomy"::: EXTPRO_1:def 12 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" (Set (Var "P"))) "iff" (Bool "(" (Bool (Set (Var "b4")) "is" (Set (Var "P")) ($#v4_extpro_1 :::"-autonomic"::: ) ) & (Bool (Set (Var "b4")) "is" (Set (Var "P")) ($#v5_extpro_1 :::"-halted"::: ) ) ")" ) ")" ))))); definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); let "d" be ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); assume (Bool (Set (Const "d")) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" (Set (Const "p"))) ; func :::"Result"::: "(" "p" "," "d" ")" -> ($#m1_hidden :::"FinPartState":::) "of" "S" means :: EXTPRO_1:def 13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" "S" "st" (Bool (Bool "p" ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" "S" "st" (Bool (Bool "d" ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "d" ")" ))))); end; :: deftheorem defines :::"Result"::: EXTPRO_1:def 13 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "d")) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" (Set (Var "p")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" )) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "d")) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "d")) ")" ))))) ")" )))))); begin definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Const "S"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::); let "d" be ($#m1_hidden :::"FinPartState":::) "of" (Set (Const "S")); let "F" be ($#m1_hidden :::"Function":::); pred "p" "," "d" :::"computes"::: "F" means :: EXTPRO_1:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"FinPartState":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set "d" ($#k1_funct_4 :::"+*"::: ) (Set (Var "s"))) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" "p") & (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_extpro_1 :::"Result"::: ) "(" "p" "," (Set "(" "d" ($#k1_funct_4 :::"+*"::: ) (Set (Var "s")) ")" ) ")" )) ")" ))); end; :: deftheorem defines :::"computes"::: EXTPRO_1:def 14 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "d")) ($#r2_extpro_1 :::"computes"::: ) (Set (Var "F"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Set (Var "d")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "s"))) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" (Set (Var "p"))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "d")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "s")) ")" ) ")" )) ")" ))) ")" )))))); theorem :: EXTPRO_1:13 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "p")) "," (Set (Var "d")) ($#r2_extpro_1 :::"computes"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))))) ; theorem :: EXTPRO_1:14 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" (Set (Var "p"))) "iff" (Bool (Set (Var "p")) "," (Set (Var "d")) ($#r2_extpro_1 :::"computes"::: ) (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k7_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "d")) ")" ")" ))) ")" ))))) ; theorem :: EXTPRO_1:15 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b2"))) ($#v5_relat_1 :::"-valued"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "d")) "is" ($#m1_extpro_1 :::"Autonomy"::: ) "of" (Set (Var "p"))) "iff" (Bool (Set (Var "p")) "," (Set (Var "d")) ($#r2_extpro_1 :::"computes"::: ) (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))))) ; begin registrationlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_memstr_0 :::"IC-Ins-separated"::: ) for ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" "N"; end; begin theorem :: EXTPRO_1:16 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "p")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )))) ")" ))))) ; theorem :: EXTPRO_1:17 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool "(" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) "iff" (Bool (Set (Var "p")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ))) ")" )))))) ; theorem :: EXTPRO_1:18 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "P")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))))) ; theorem :: EXTPRO_1:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b4"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "P")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Var "P")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "j")) ")" ")" )))))))) ; theorem :: EXTPRO_1:20 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_zero"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b4"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "P")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ))))))) ; theorem :: EXTPRO_1:21 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "P")) ($#r1_compos_1 :::"halts_at"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ")" ))))))) ; definitionlet "N" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "p" 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":::); let "s" be ($#m1_hidden :::"State":::) "of" (Set (Const "S")); assume (Bool (Set (Const "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Const "s"))) ; func :::"LifeSpan"::: "(" "p" "," "s" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: EXTPRO_1:def 15 (Bool "(" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" "p" "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" "p" "," "s" "," it ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" "p" "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" "p" "," "s" "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) "S"))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ); end; :: deftheorem defines :::"LifeSpan"::: EXTPRO_1:def 15 : (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "b5")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "b5")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ) ")" )))))); theorem :: EXTPRO_1:22 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) "iff" (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "m")) ")" )) ")" )))))) ; theorem :: EXTPRO_1:23 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (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":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" )))))) ; theorem :: EXTPRO_1:24 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))))) ; theorem :: EXTPRO_1:25 (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set (Var "b3"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ))))))) ; theorem :: EXTPRO_1:26 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "e")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "e")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "u")))) "holds" (Bool (Set ($#k4_extpro_1 :::"Following"::: ) "(" (Set (Var "u")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "t")) ")" )))))))) ; theorem :: EXTPRO_1:27 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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")) ($#r1_hidden :::"="::: ) (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")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s")))))))) ; theorem :: EXTPRO_1:28 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k4_extpro_1 :::"Following"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" )))))))) ; theorem :: EXTPRO_1:29 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) ")" ))))) ; theorem :: EXTPRO_1:30 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "F")) "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 "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))))) "holds" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))))) ; theorem :: EXTPRO_1:31 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))))) ; theorem :: EXTPRO_1:32 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S")))) "iff" (Bool "(" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) ")" ) ")" )))))) ; theorem :: EXTPRO_1:33 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))))))) ; theorem :: EXTPRO_1:34 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ")" )))))))) ; theorem :: EXTPRO_1:35 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))) "holds" (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ))))))) ; theorem :: EXTPRO_1:36 (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set (Var "S"))))))))) ;