:: SCM_HALT semantic presentation begin definitionlet "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); attr "I" is :::"InitClosed"::: means :: SCM_HALT:def 1 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "I" ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "I"))))); attr "I" is :::"InitHalting"::: means :: SCM_HALT:def 2 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "I" ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))); attr "I" is :::"keepInt0_1"::: means :: SCM_HALT:def 3 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "I" ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))))); end; :: deftheorem defines :::"InitClosed"::: SCM_HALT:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_scm_halt :::"InitClosed"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "I"))))))) ")" )); :: deftheorem defines :::"InitHalting"::: SCM_HALT:def 2 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))) ")" )); :: deftheorem defines :::"keepInt0_1"::: SCM_HALT:def 3 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v3_scm_halt :::"keepInt0_1"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))))) ")" )); theorem :: SCM_HALT:1 canceled; theorem :: SCM_HALT:2 (Bool (Set ($#k11_compos_1 :::"Macro"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() bbbadV2_PRE_POLY() ($#v2_scm_halt :::"InitHalting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v6_amistd_1 :::"paraclosed"::: ) -> ($#v1_scm_halt :::"InitClosed"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v7_amistd_1 :::"parahalting"::: ) -> ($#v2_scm_halt :::"InitHalting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v2_scm_halt :::"InitHalting"::: ) -> ($#v1_scm_halt :::"InitClosed"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v3_scm_halt :::"keepInt0_1"::: ) -> ($#v1_scm_halt :::"InitClosed"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v1_scmfsa6b :::"keeping_0"::: ) -> ($#v3_scm_halt :::"keepInt0_1"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCM_HALT:3 canceled; theorem :: SCM_HALT:4 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCM_HALT:5 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))))))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v2_scm_halt :::"InitHalting"::: ) -> for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCM_HALT:6 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "J")) ($#r1_tarski :::"c="::: ) (Set (Var "p1")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "J")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "p2"))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) ")" )))))) ; theorem :: SCM_HALT:7 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p2"))) & (Bool (Set (Var "s1")) ($#r8_pboole :::"="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "p2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SCM_HALT:8 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p2"))) & (Bool (Set (Var "s1")) ($#r8_pboole :::"="::: ) (Set (Var "s2")))) "holds" (Bool "(" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) ")" )) & (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) ")" )) ")" )))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v1_scmfsa6b :::"keeping_0"::: ) bbbadV2_PRE_POLY() ($#v2_scm_halt :::"InitHalting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() bbbadV2_PRE_POLY() ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCM_HALT:9 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() bbbadV2_PRE_POLY() ($#v1_scm_halt :::"InitClosed"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCM_HALT:10 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scm_halt :::"InitClosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "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 ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "m")) ")" ))))))) ; theorem :: SCM_HALT:11 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scm_halt :::"InitClosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I"))) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) & (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: SCM_HALT:12 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scm_halt :::"InitClosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I"))) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) & (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )))))) ; theorem :: SCM_HALT:13 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))))) ; theorem :: SCM_HALT:14 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scm_halt :::"InitClosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I"))) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))))) "holds" (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ))))))) ; theorem :: SCM_HALT:15 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ))) & (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "J")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ))) & "(" (Bool (Bool (Set (Var "J")) "is" ($#v1_scmfsa6b :::"keeping_0"::: ) )) "implies" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ))))) ; registrationlet "I" be ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "I" ($#k3_scmfsa6a :::"";""::: ) "J") -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; theorem :: SCM_HALT:16 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I"))) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "J")) "being" ($#v1_scm_halt :::"InitClosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" )) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set (Var "s")) "," (Set "(" (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ))))))) ; theorem :: SCM_HALT:17 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I"))) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")))))) "holds" (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ))))))) ; theorem :: SCM_HALT:18 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ))))))) ; theorem :: SCM_HALT:19 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" )))))) ; registrationlet "i" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k11_compos_1 :::"Macro"::: ) "i") -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; registrationlet "i" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "i" ($#k4_scmfsa6a :::"";""::: ) "J") -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; registrationlet "i" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#v2_scmfsa6c :::"keeping_0"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "i" ($#k4_scmfsa6a :::"";""::: ) "J") -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; registrationlet "I", "J" be ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "I" ($#k3_scmfsa6a :::"";""::: ) "J") -> ($#v3_scm_halt :::"keepInt0_1"::: ) ; end; registrationlet "j" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#v2_scmfsa6c :::"keeping_0"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "I" be ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "I" ($#k5_scmfsa6a :::"";""::: ) "j") -> ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ; end; registrationlet "i" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#v2_scmfsa6c :::"keeping_0"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "i" ($#k4_scmfsa6a :::"";""::: ) "J") -> ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ; end; registrationlet "j" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "I" be ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "I" ($#k5_scmfsa6a :::"";""::: ) "j") -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; registrationlet "i", "j" be ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "i" ($#k6_scmfsa6a :::"";""::: ) "j") -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; theorem :: SCM_HALT:20 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCM_HALT:21 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SCM_HALT:22 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )))))) ; theorem :: SCM_HALT:23 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCM_HALT:24 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; definitionlet "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "p" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); pred "I" :::"is_closed_onInit"::: "s" "," "p" means :: SCM_HALT:def 4 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "p" ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) "s" ")" ) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "I"))); pred "I" :::"is_halting_onInit"::: "s" "," "p" means :: SCM_HALT:def 5 (Bool (Set "p" ($#k1_funct_4 :::"+*"::: ) "I") ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) "s")); end; :: deftheorem defines :::"is_closed_onInit"::: SCM_HALT:def 4 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "I"))))) ")" )))); :: deftheorem defines :::"is_halting_onInit"::: SCM_HALT:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I"))) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")))) ")" )))); theorem :: SCM_HALT:25 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_scm_halt :::"InitClosed"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))))) ")" )) ; theorem :: SCM_HALT:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))))) ")" )) ; theorem :: SCM_HALT:27 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v1_scmfsa7b :::"good"::: ) bbbadV2_PRE_POLY() ($#v2_scm_halt :::"InitHalting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v1_scmfsa7b :::"good"::: ) ($#v1_scm_halt :::"InitClosed"::: ) -> ($#v3_scm_halt :::"keepInt0_1"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) -> ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ; end; theorem :: SCM_HALT:28 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#v2_scmfsa6c :::"keeping_0"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCM_HALT:29 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v1_scmfsa6c :::"parahalting"::: ) ($#v2_scmfsa6c :::"keeping_0"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SCM_HALT:30 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" )))) ; theorem :: SCM_HALT:31 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) "iff" (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))) ")" )))) ; theorem :: SCM_HALT:32 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))))) ; theorem :: SCM_HALT:33 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) ")" ))))) ; theorem :: SCM_HALT:34 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:35 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) ")" ))))) ; theorem :: SCM_HALT:36 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:37 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) ")" ")" ))))) ; theorem :: SCM_HALT:38 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" ")" ))))) ; theorem :: SCM_HALT:39 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) ")" ))))) ; theorem :: SCM_HALT:40 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:41 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) ")" ))))) ; theorem :: SCM_HALT:42 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:43 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) ")" ")" ))))) ; theorem :: SCM_HALT:44 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" ")" ))))) ; theorem :: SCM_HALT:45 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k3_scmfsa8b :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 7) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:46 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k3_scmfsa8b :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 7) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:47 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "J")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "J")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k3_scmfsa8b :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 7) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))))))) ; theorem :: SCM_HALT:48 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set ($#k3_scmfsa8b :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k3_scmfsa8b :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 7) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k3_scmfsa8b :::"if<0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 7) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" ))) ")" ")" ))))) ; registrationlet "I", "J" be ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); cluster (Set ($#k1_scmfsa8b :::"if=0"::: ) "(" "a" "," "I" "," "J" ")" ) -> ($#v2_scm_halt :::"InitHalting"::: ) ; cluster (Set ($#k2_scmfsa8b :::"if>0"::: ) "(" "a" "," "I" "," "J" ")" ) -> ($#v2_scm_halt :::"InitHalting"::: ) ; cluster (Set ($#k3_scmfsa8b :::"if<0"::: ) "(" "a" "," "I" "," "J" ")" ) -> ($#v2_scm_halt :::"InitHalting"::: ) ; end; theorem :: SCM_HALT:49 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))))) ")" )) ; theorem :: SCM_HALT:50 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_scm_halt :::"InitClosed"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))))) ")" )) ; theorem :: SCM_HALT:51 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCM_HALT:52 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCM_HALT:53 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCM_HALT:54 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v3_scm_halt :::"keepInt0_1"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))))))) ; theorem :: SCM_HALT:55 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scm_halt :::"InitClosed"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))) "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 ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "m")) ")" )))))) ; theorem :: SCM_HALT:56 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))))))) ; theorem :: SCM_HALT:57 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "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 ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" )))))) ; theorem :: SCM_HALT:58 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "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 ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ")" ) ")" )))))) ; theorem :: SCM_HALT:59 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "p")))) "holds" (Bool "(" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (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 ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "m")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ")" ) ")" )))) ; theorem :: SCM_HALT:60 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "p"))))))) ; theorem :: SCM_HALT:61 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "p"))))))) ; theorem :: SCM_HALT:62 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "p"))) & (Bool (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "p"))) ")" ))))) ; theorem :: SCM_HALT:63 (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_scmfsa_3 :::".-->"::: ) (Num 1) ")" )) "is" (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#v5_extpro_1 :::"-halted"::: ) ))) ; registrationlet "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); let "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k2_scmfsa8c :::"Times"::: ) "(" "a" "," "I" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; theorem :: SCM_HALT:64 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )(Bool "ex" (Set (Var "p2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s2")) ($#r8_pboole :::"="::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")))) & (Bool (Set (Var "p2")) ($#r8_pboole :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "b")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_scmfsa8c :::"loop"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ))) ")" ) ")" )))))))) ; theorem :: SCM_HALT:65 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s")))))))) ; theorem :: SCM_HALT:66 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ))) ")" ))))) ; theorem :: SCM_HALT:67 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SCM_HALT:68 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; theorem :: SCM_HALT:69 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SCM_HALT:70 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "p")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; definitionlet "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); redefine attr "i" is :::"good"::: means :: SCM_HALT:def 6 (Bool (Bool "not" "i" ($#r3_scmfsa7b :::"destroys"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) )))); end; :: deftheorem defines :::"good"::: SCM_HALT:def 6 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#v1_sfmastr1 :::"good"::: ) ) "iff" (Bool (Bool "not" (Set (Var "i")) ($#r3_scmfsa7b :::"destroys"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ")" ));