:: SCMBSORT semantic presentation begin theorem :: SCMBSORT:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Bool "not" (Set (Var "I")) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "not" (Bool (Set ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "b")))))) ; theorem :: SCMBSORT:2 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" )))))) ; theorem :: SCMBSORT:3 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: SCMBSORT:4 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "m")) "," (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 (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "m")) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))))) ; theorem :: SCMBSORT:5 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "m")) "," (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 (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set (Var "m")) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: SCMBSORT:6 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ))))) ; theorem :: SCMBSORT:7 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "ic")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool "(" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")))) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))) ")" )))) ; theorem :: SCMBSORT:8 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "ic")) "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 "la")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "ic")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool "(" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "la")))) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "la")))) ")" )) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))))))) ; theorem :: SCMBSORT:9 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "ic")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool "(" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "fa")) "," (Set (Var "a")) ")" )) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))) ")" ))))) ; theorem :: SCMBSORT:10 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "ic")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool "(" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "fa")) "," (Set (Var "a")) ")" )) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "fa")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set (Var "fa")) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")))))))) ; theorem :: SCMBSORT:11 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "ic")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool "(" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "fa")))) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fa")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))))))) ; theorem :: SCMBSORT:12 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "fa")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "ic")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))) & (Bool "(" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "fa")))) "or" (Bool (Set (Var "ic")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fa")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "fa")) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")))))))) ; theorem :: SCMBSORT:13 (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "x")) "is" (Bool "not" ($#m1_subset_1 :::"Int-Location":::)))) "holds" (Bool (Set (Var "x")) "is" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) )))) ; theorem :: SCMBSORT:14 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "p2"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "j")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "j")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) ")" ) ")" ) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" ))) ")" )))))) ; theorem :: SCMBSORT:15 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "p2"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "j")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "j")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) ")" ) ")" ) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "k")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ))) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "p2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ")" ))) ")" ))))) ; theorem :: SCMBSORT:16 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa8b :::"if=0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ))) & (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) "," (Set (Var "J")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ))) ")" ))) ; theorem :: SCMBSORT:17 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "I")) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")))))) ; theorem :: SCMBSORT:18 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k5_scmfsa_m :::"}"::: ) ))))) ; theorem :: SCMBSORT:19 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k1_scmfsa6a :::"Directed"::: ) "(" (Set (Var "I")) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")))))) ; theorem :: SCMBSORT:20 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")))))) ; theorem :: SCMBSORT:21 canceled; theorem :: SCMBSORT:22 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 12))))) ; theorem :: SCMBSORT:23 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "i1")) ($#k6_scmfsa6a :::"";""::: ) (Set (Var "i2")) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "i3")) ")" )) ($#r1_hidden :::"="::: ) (Num 6))) ; theorem :: SCMBSORT:24 canceled; theorem :: SCMBSORT:25 canceled; theorem :: SCMBSORT:26 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "J")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ))))) ; theorem :: SCMBSORT:27 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "i")) "being" ($#v4_compos_0 :::"ins-loc-free"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "i")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; theorem :: SCMBSORT:28 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "i")) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))))) ; theorem :: SCMBSORT:29 canceled; theorem :: SCMBSORT:30 canceled; theorem :: SCMBSORT:31 canceled; theorem :: SCMBSORT:32 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s")))))) ; theorem :: SCMBSORT:33 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))))))) ; definitionlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; func :::"bubble-sort"::: "f" -> ($#m1_hidden :::"Program":::) "of" equals :: SCMBSORT:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ($#k16_scmfsa_2 :::":=len"::: ) "f" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ($#k16_scmfsa_2 :::":=len"::: ) "f" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"bubble-sort"::: SCMBSORT:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k1_scmbsort :::"bubble-sort"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )))); definitionfunc :::"Bubble-Sort-Algorithm"::: -> ($#m1_hidden :::"Program":::) "of" equals :: SCMBSORT:def 2 (Set ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )); end; :: deftheorem defines :::"Bubble-Sort-Algorithm"::: SCMBSORT:def 2 : (Bool (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))); theorem :: SCMBSORT:34 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k1_scmbsort :::"bubble-sort"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k5_enumset1 :::"}"::: ) ))) ; theorem :: SCMBSORT:35 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k1_scmbsort :::"bubble-sort"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SCMBSORT:36 canceled; theorem :: SCMBSORT:37 canceled; theorem :: SCMBSORT:38 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_scmbsort :::"bubble-sort"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Num 63))) ; theorem :: SCMBSORT:39 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Num 63))) "holds" (Bool (Set (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: SCMBSORT:40 (Bool "(" (Bool (Set ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#v3_scm_halt :::"keepInt0_1"::: ) ) & (Bool (Set ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) ")" ) ; theorem :: SCMBSORT:41 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) "," (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k1_scmbsort :::"bubble-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "x2")))) ")" ) ")" ))) ; theorem :: SCMBSORT:42 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "w")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ))))))) ; theorem :: SCMBSORT:43 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "t")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "t")) "," (Set (Var "u")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set (Var "u")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Var "u")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) )) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "p")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "u"))) ")" ))))) ; theorem :: SCMBSORT:44 (Bool "for" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "w")) ")" )) "is" (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) ($#v4_extpro_1 :::"-autonomic"::: ) )) ; registration cluster (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) -> ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; theorem :: SCMBSORT:45 (Bool (Set ($#k2_scmbsort :::"Bubble-Sort-Algorithm"::: ) ) "," (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) ($#r2_extpro_1 :::"computes"::: ) (Set ($#k10_scmfsa_m :::"Sorting-Function"::: ) )) ;