:: SCM_1 semantic presentation begin definitionlet "i" be ($#m1_hidden :::"Integer":::); :: original: :::"<*"::: redefine func :::"<*":::"i":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "i1" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k3_afinsq_1 :::"<%"::: ) "i1" ($#k3_afinsq_1 :::"%>"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; let "i2" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k6_afinsq_1 :::"<%"::: ) "i1" "," "i2" ($#k6_afinsq_1 :::"%>"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; let "i3" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k7_afinsq_1 :::"<%"::: ) "i1" "," "i2" "," "i3" ($#k7_afinsq_1 :::"%>"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; let "i4" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k16_afinsq_1 :::"<%"::: ) "i1" "," "i2" "," "i3" "," "i4" ($#k16_afinsq_1 :::"%>"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "D" be ($#m1_hidden :::"XFinSequence":::) "of" (Set ($#k4_numbers :::"INT"::: ) ); mode :::"State-consisting"::: "of" "D" -> ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) means :: SCM_1:def 1 (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 ($#k1_afinsq_1 :::"len"::: ) "D"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set "D" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))); end; :: deftheorem defines :::"State-consisting"::: SCM_1:def 1 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set (Var "D"))) "iff" (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 ($#k1_afinsq_1 :::"len"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) ")" ))); registrationlet "D" be ($#m1_hidden :::"XFinSequence":::) "of" (Set ($#k4_numbers :::"INT"::: ) ); let "il" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster bbbadV1_XBOOLE_0() ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) (Set ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_funct_1 :::"-compatible"::: ) ($#v1_partfun1 :::"total"::: ) "il" ($#v5_memstr_0 :::"-started"::: ) for ($#m1_scm_1 :::"State-consisting"::: ) "of" "D"; end; theorem :: SCM_1:1 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "il")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set (Var "b5")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) ($#k16_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i1"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i3"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i4"))) ")" )))) ; theorem :: SCM_1:2 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "il")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set (Var "b3")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i1"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) ")" )))) ; theorem :: SCM_1:3 (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "I1")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "I2")) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "I1"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "I2"))) ")" ))) ; theorem :: SCM_1:4 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b"))))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))))) ; theorem :: SCM_1:5 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))))) ; theorem :: SCM_1:6 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))))) ; theorem :: SCM_1:7 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))))) ; theorem :: SCM_1:8 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))))) ; theorem :: SCM_1:9 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "il")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "il"))))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "il"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ))))) ; theorem :: SCM_1:10 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "il")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "il"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "il"))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))))) ; theorem :: SCM_1:11 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "il")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "F")) ($#k3_compos_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "il"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "il"))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))))) ; theorem :: SCM_1:12 (Bool "(" (Bool (Set (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b")) ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 5)) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "i")) ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 6)) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "i")) ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 7))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "i")) ")" ) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 8))) ")" ) ")" ) ; theorem :: SCM_1:13 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i1"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i3"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i4")))) "holds" (Bool (Set (Var "s")) "is" ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "," (Set (Var "i4")) ($#k16_afinsq_1 :::"%>"::: ) )))) ; theorem :: SCM_1:14 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ))) ; theorem :: SCM_1:15 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i2"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:16 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i2")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:17 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i2")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:18 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i2")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:19 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k5_int_1 :::"div"::: ) (Set (Var "i2")))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k6_int_1 :::"mod"::: ) (Set (Var "i2")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:20 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Num 1) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:21 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 1) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:22 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k9_ami_3 :::">0_goto"::: ) (Num 1) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "i1")) "," (Set (Var "i2")) ($#k6_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" )))) ; theorem :: SCM_1:23 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool (Set (Var "s")) "is" ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k4_numbers :::"INT"::: ) )))) ;