:: SCMFSA6B semantic presentation begin definitionlet "I" be ($#m1_hidden :::"Program":::) "of" ; 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"::: ) ); func :::"IExec"::: "(" "I" "," "P" "," "s" ")" -> ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA6B:def 1 (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) "s" ")" ) ")" ); end; :: deftheorem defines :::"IExec"::: SCMFSA6B:def 1 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (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 ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ))))); definitionlet "I" be ($#m1_hidden :::"Program":::) "of" ; canceled; canceled; attr "I" is :::"keeping_0"::: means :: SCMFSA6B:def 4 (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#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 "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 :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))))); end; :: deftheorem SCMFSA6B:def 2 : canceled; :: deftheorem SCMFSA6B:def 3 : canceled; :: deftheorem defines :::"keeping_0"::: SCMFSA6B:def 4 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_scmfsa6b :::"keeping_0"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#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 "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 :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))))) ")" )); registration cluster ($#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_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v7_amistd_1 :::"parahalting"::: ) bbbadV2_PRE_POLY() ($#v1_scmfsa6b :::"keeping_0"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCMFSA6B:1 (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (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")))))) ; theorem :: SCMFSA6B:2 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (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")))))) ; registration cluster ($#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_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v7_amistd_1 :::"parahalting"::: ) -> ($#v6_amistd_1 :::"paraclosed"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v1_scmfsa6b :::"keeping_0"::: ) -> ($#v6_amistd_1 :::"paraclosed"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCMFSA6B:3 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (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 :: SCMFSA6B:4 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "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")))))))) ; theorem :: SCMFSA6B:5 (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "l"))) & (Bool (Set (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l"))))) "holds" (Bool "not" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))))))) ; registration cluster ($#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_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v7_amistd_1 :::"parahalting"::: ) -> for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCMFSA6B:6 (Bool "for" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s1")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (Bool (Set (Var "J")) ($#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 ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "J")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (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 "P")) "," (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 "Q")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "Q")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ))) ")" ))))))) ; theorem :: SCMFSA6B:7 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "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 "s")) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SCMFSA6B:8 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "(" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) & (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) ")" )))) ; theorem :: SCMFSA6B:9 canceled; theorem :: SCMFSA6B:10 canceled; theorem :: SCMFSA6B: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" ($#v7_amistd_1 :::"parahalting"::: ) ($#v1_scmfsa6b :::"keeping_0"::: ) ($#m1_hidden :::"Program":::) "of" "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))))) ; begin registration cluster ($#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_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v6_amistd_1 :::"paraclosed"::: ) bbbadV2_PRE_POLY() for ($#m1_hidden :::"set"::: ) ; end; theorem :: SCMFSA6B:12 (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v6_amistd_1 :::"paraclosed"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (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"))) & (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 :: SCMFSA6B:13 (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#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" ($#v6_amistd_1 :::"paraclosed"::: ) ($#m1_hidden :::"Program":::) "of" "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")))) "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 :: SCMFSA6B:14 (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#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" ($#v6_amistd_1 :::"paraclosed"::: ) ($#m1_hidden :::"Program":::) "of" "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")))) "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 :: SCMFSA6B:15 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (Bool (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"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "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 :: SCMFSA6B:16 (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#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" ($#v6_amistd_1 :::"paraclosed"::: ) ($#m1_hidden :::"Program":::) "of" "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" ($#m1_hidden :::"Program":::) "of" (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 (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (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 (Var "s")) "," (Set (Var "k")) ")" ))))))) ; registrationlet "I", "J" be ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" ; cluster (Set "I" ($#k3_scmfsa6a :::"";""::: ) "J") -> ($#v7_amistd_1 :::"parahalting"::: ) ; end; theorem :: SCMFSA6B:17 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa6b :::"keeping_0"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (Bool (Bool "not" (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" ($#m1_hidden :::"Program":::) "of" (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 (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 (Var "s")) "," (Set (Var "k")) ")" ))))))) ; theorem :: SCMFSA6B:18 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v1_scmfsa6b :::"keeping_0"::: ) ($#m1_hidden :::"Program":::) "of" "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" ($#v6_amistd_1 :::"paraclosed"::: ) ($#m1_hidden :::"Program":::) "of" "st" (Bool (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 ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ) ($#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")) ")" ) ")" ))))))) ; registrationlet "I", "J" be ($#v1_scmfsa6b :::"keeping_0"::: ) ($#m1_hidden :::"Program":::) "of" ; cluster (Set "I" ($#k3_scmfsa6a :::"";""::: ) "J") -> ($#v1_scmfsa6b :::"keeping_0"::: ) ; end; theorem :: SCMFSA6B: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" ($#v7_amistd_1 :::"parahalting"::: ) ($#v1_scmfsa6b :::"keeping_0"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "J")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ) ($#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 "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ))))))) ; theorem :: SCMFSA6B:20 (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" ($#v7_amistd_1 :::"parahalting"::: ) ($#v1_scmfsa6b :::"keeping_0"::: ) ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "J")) "being" ($#v7_amistd_1 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" "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")) ")" ) ")" )))))) ; theorem :: SCMFSA6B:21 (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 "not" (Set (Set (Var "P")) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" ) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s")))))) ;