:: SCMFSA8A semantic presentation begin theorem :: SCMFSA8A:1 canceled; theorem :: SCMFSA8A:2 canceled; theorem :: SCMFSA8A:3 canceled; theorem :: SCMFSA8A:4 canceled; theorem :: SCMFSA8A:5 canceled; theorem :: SCMFSA8A:6 canceled; theorem :: SCMFSA8A:7 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) "implies" (Bool (Set (Set "(" ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "P")) "," (Set (Var "l")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")))) ")" & "(" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) "implies" (Bool (Set (Set "(" ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "P")) "," (Set (Var "l")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ")" )))) ; theorem :: SCMFSA8A:8 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) ")" ) ($#r3_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))))) ; theorem :: SCMFSA8A:9 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "P")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "P")) "," (Set (Var "n")) ")" ) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))))) ; theorem :: SCMFSA8A:10 (Bool "for" (Set (Var "P")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "P")) "," (Set (Var "n")) ")" ) "is" ($#v1_scmfsa7b :::"good"::: ) ))) ; theorem :: SCMFSA8A:11 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"preProgram":::) "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 (Bool "not" (Set (Var "J")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))) "holds" (Bool "not" (Bool (Set (Set (Var "I")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J"))) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a")))))) ; theorem :: SCMFSA8A:12 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J"))) "is" ($#v1_scmfsa7b :::"good"::: ) )) ; theorem :: SCMFSA8A:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "not" (Bool (Set ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "I")) "," (Set (Var "l")) ")" ) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "a"))))))) ; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_scmfsa6a :::"Directed"::: ) "(" "I" "," "l" ")" ) -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "I" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k2_scmfsa6a :::"Directed"::: ) "I") -> ($#v1_scmfsa7b :::"good"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_scmfsa6a :::"Directed"::: ) "(" "I" "," "l" ")" ) -> ($#v1_afinsq_1 :::"initial"::: ) ; end; registrationlet "I", "J" be ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set "I" ($#k3_scmfsa6a :::"";""::: ) "J") -> ($#v1_scmfsa7b :::"good"::: ) ; end; definitionlet "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Goto"::: "l" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA8A:def 1 (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) "l" ")" )); end; :: deftheorem defines :::"Goto"::: SCMFSA8A:def 1 : (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_scmfsa8a :::"Goto"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")) ")" )))); registrationlet "l" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_scmfsa8a :::"Goto"::: ) "l") -> ($#v2_compos_1 :::"halt-free"::: ) ($#v1_scmfsa7b :::"good"::: ) ; 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"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) bbbadV1_FINSET_1() ($#v1_afinsq_1 :::"initial"::: ) ($#v2_compos_1 :::"halt-free"::: ) ($#v1_scmfsa7b :::"good"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "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"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); pred "I" :::"is_pseudo-closed_on"::: "s" "," "P" means :: SCMFSA8A:def 2 (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) "s" ")" ) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) "I")) & (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 "(" "P" ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) "s" ")" ) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) "I")) ")" ) ")" )); end; :: deftheorem defines :::"is_pseudo-closed_on"::: SCMFSA8A:def 2 : (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))) & (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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))) ")" ) ")" )) ")" )))); registration cluster ($#v1_amistd_2 :::"with_explicit_jumps"::: ) ($#v3_amistd_2 :::"IC-relocable"::: ) ($#v4_amistd_1 :::"sequential"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); end; definitioncanceled; 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"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); assume (Bool (Set (Const "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Const "s")) "," (Set (Const "P"))) ; func :::"pseudo-LifeSpan"::: "(" "s" "," "P" "," "I" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SCMFSA8A:def 4 (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) "s" ")" ) "," it ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) "I")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) "s" ")" ) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) "I")))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ); end; :: deftheorem SCMFSA8A:def 3 : canceled; :: deftheorem defines :::"pseudo-LifeSpan"::: SCMFSA8A:def 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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set (Var "I")) ")" )) "iff" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "b4")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) ")" ))))); theorem :: SCMFSA8A:14 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: SCMFSA8A:15 (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SCMFSA8A:16 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "P"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) "implies" (Bool (Set (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "P")) ")" ))) ")" & "(" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) "implies" (Bool (Set (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ")" ))) ; theorem :: SCMFSA8A: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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (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 ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set (Var "I")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set (Var "I")))) & (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 "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ")" ))))) ; theorem :: SCMFSA8A: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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (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 ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set (Var "I")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" )))))) ; theorem :: SCMFSA8A:19 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "I")) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))))) ; theorem :: SCMFSA8A:20 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))) ; theorem :: SCMFSA8A: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"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" )) & (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 "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ")" ))))) ; theorem :: SCMFSA8A:22 (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (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 "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" )))) ; theorem :: SCMFSA8A:23 (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I"))) ($#r1_scmfsa8a :::"is_pseudo-closed_on"::: ) (Set (Var "s")) "," (Set (Var "P")))))) ; theorem :: SCMFSA8A:24 (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set ($#k2_scmfsa8a :::"pseudo-LifeSpan"::: ) "(" (Set (Var "s")) "," (Set (Var "P")) "," (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: SCMFSA8A:25 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J"))))) ; theorem :: SCMFSA8A:26 (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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (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 "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ))) & (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 "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ) ")" ) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" )))) ; theorem :: SCMFSA8A:27 (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")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool "(" (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 "(" (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) ")" ) ")" ) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ))) & (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 "(" (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ) ")" ) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" ))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" ))) ")" )))) ; theorem :: SCMFSA8A:28 (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (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 "(" (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) ")" ) ")" ) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" )) & (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 "(" (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) ")" ) ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) ")" ))))) ; theorem :: SCMFSA8A:29 (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" ))) ")" )))) ; theorem :: SCMFSA8A:30 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))) ; theorem :: SCMFSA8A:31 (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set (Var "l")) ")" ))) & (Bool (Set (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set (Var "l")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")))) ")" )) ; theorem :: SCMFSA8A:32 (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"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: SCMFSA8A:33 (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"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ) ")" ) "," (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) ")" ) ")" ")" )))))) ; theorem :: SCMFSA8A:34 (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"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" )) ($#r1_extpro_1 :::"halts_on"::: ) (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) ")" ) ")" )))))) ; theorem :: SCMFSA8A:35 (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"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) ")" ) "," (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 "(" ($#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)))))) ; theorem :: SCMFSA8A:36 (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" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (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 "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" )))))) ; theorem :: SCMFSA8A:37 (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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" )))) ; theorem :: SCMFSA8A:38 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "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"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set (Var "s")) "," (Set (Var "P")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" )) ($#r1_extpro_1 :::"halts_on"::: ) (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s"))))))) ; theorem :: SCMFSA8A:39 (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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" )) ($#r1_extpro_1 :::"halts_on"::: ) (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) ")" ) ")" )))))) ; theorem :: SCMFSA8A:40 (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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (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 1)))))) ; theorem :: SCMFSA8A:41 (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 "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r5_scmfsa7b :::"is_closed_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool (Set ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" (Set "(" (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "J")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (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 1) ")" ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ")" )))))) ;