:: SCMISORT semantic presentation begin theorem :: SCMISORT:1 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool "ex" (Set (Var "pc")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool "(" (Bool (Set (Var "pc")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) & (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "pc"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "ic")))) ")" ))) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "l")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "ic")) ")" ) ")" )))))) ; theorem :: SCMISORT:2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k1_scmfsa8a :::"Goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) "," (Set "(" ($#k4_compos_1 :::"Stop"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ))))) ; theorem :: SCMISORT:3 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ic")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool "ex" (Set (Var "pc")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool "(" (Bool (Set (Var "pc")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) & (Bool (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "pc"))) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "ic")))) ")" ))) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "l")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "ic")) ")" ) ")" )))))) ; theorem :: SCMISORT:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (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"))))) "holds" (Bool "not" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r4_scmfsa7b :::"destroys"::: ) (Set (Var "b")))))) ; theorem :: SCMISORT:5 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r6_scmfsa7b :::"is_halting_on"::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s"))) "," (Set (Var "P")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMISORT:6 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "k")) ")" )) & (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P2")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" )) ")" ))))) ; theorem :: SCMISORT:7 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "(" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) & (Bool (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P1")) "," (Set (Var "s")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) ")" )))) ; begin theorem :: SCMISORT:8 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCMISORT:9 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" )) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" )))))) ; theorem :: SCMISORT:10 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4)))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ))))))) ; theorem :: SCMISORT:11 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3)))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) ")" ) ")" ))))) ; theorem :: SCMISORT:12 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3)))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" )))))))) ; theorem :: SCMISORT:13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ")" ")" ))) ")" ))))) ; theorem :: SCMISORT:14 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s2")) ($#r8_pboole :::"="::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set (Var "s2")) "," (Set (Var "k")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))))))) ; definitionlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "I" be ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "a" be ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::); let "P" be ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"StepWhile>0"::: "(" "a" "," "P" "," "s" "," "I" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) means :: SCMISORT:def 1 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r8_pboole :::"="::: ) "s") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" "a" "," "I" ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" "P" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" "a" "," "I" ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) "I" ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"StepWhile>0"::: SCMISORT:def 1 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r8_pboole :::"="::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )) ")" ) ")" ) ")" )))))); theorem :: SCMISORT:15 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Num 1)))))))) ; theorem :: SCMISORT:16 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" )))))) ; theorem :: SCMISORT:17 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" )) & (Bool (Set (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r8_pboole :::"="::: ) (Set ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ))) & (Bool (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "I")) ")" ) "," (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" )) ")" )))))) ; theorem :: SCMISORT:18 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ))) & (Bool (Set (Var "I")) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) "," (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Set (Var "I")) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) "," (Set (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ))) ")" ) ")" & (Bool (Set (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & "(" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_scmisort :::"StepWhile>0"::: ) "(" (Set (Var "a")) "," (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "I")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r2_scm_halt :::"is_halting_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) & (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) ($#r1_scm_halt :::"is_closed_onInit"::: ) (Set (Var "s")) "," (Set (Var "P"))) ")" ))))) ; theorem :: SCMISORT:19 (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool "(" "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 (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" )) "holds" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) ))) ; theorem :: SCMISORT:20 (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) "or" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )) "holds" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) ))) ; theorem :: SCMISORT:21 (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_memstr_0 :::"the_Values_of"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ")" ) "," (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" & "(" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "t"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")))) ")" & "(" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))))) "holds" (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) ))) ; theorem :: SCMISORT:22 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ))))))) ; theorem :: SCMISORT:23 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) )) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ")" ))))))) ; theorem :: SCMISORT:24 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SCMISORT:25 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa_m :::"Initialized"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; theorem :: SCMISORT:26 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SCMISORT:27 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scm_halt :::"InitHalting"::: ) ($#v1_scmfsa7b :::"good"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "a")) "being" ($#v1_scmfsa_m :::"read-write"::: ) ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ) "is" ($#v2_scm_halt :::"InitHalting"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set (Var "a")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "P")) "," (Set "(" ($#k1_scmfsa6b :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))))))))) ; begin definitionlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; func :::"insert-sort"::: "f" -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMISORT:def 2 (Set (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" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#k16_scmfsa_2 :::":=len"::: ) "f" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (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 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) "," (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#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 2) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"insert-sort"::: SCMISORT:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k2_scmisort :::"insert-sort"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (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")) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")) ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (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 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa_9 :::"while>0"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8b :::"if>0"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) "," (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ")" ) ")" ) "," (Set "(" (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ($#k6_scmfsa6a :::"";""::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ($#k3_scmfsa6a :::"";""::: ) (Set "(" ($#k2_scmfsa8c :::"Times"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ($#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 2) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 6) ")" ) ")" ) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set "(" "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 3) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 5) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" )))); definitionfunc :::"Insert-Sort-Algorithm"::: -> ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMISORT:def 3 (Set ($#k2_scmisort :::"insert-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )); end; :: deftheorem defines :::"Insert-Sort-Algorithm"::: SCMISORT:def 3 : (Bool (Set ($#k3_scmisort :::"Insert-Sort-Algorithm"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_scmisort :::"insert-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))); theorem :: SCMISORT:28 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k2_scmisort :::"insert-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 :: SCMISORT:29 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k2_scmisort :::"insert-sort"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SCMISORT:30 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "," (Set (Var "k3")) "," (Set (Var "k4")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "k1")) ($#k6_scmfsa6a :::"";""::: ) (Set (Var "k2")) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "k3")) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "k4")) ")" )) ($#r1_hidden :::"="::: ) (Num 8))) ; theorem :: SCMISORT:31 (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "," (Set (Var "k3")) "," (Set (Var "k4")) "," (Set (Var "k5")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "k1")) ($#k6_scmfsa6a :::"";""::: ) (Set (Var "k2")) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "k3")) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "k4")) ")" ) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "k5")) ")" )) ($#r1_hidden :::"="::: ) (Num 10))) ; theorem :: SCMISORT:32 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_scmisort :::"insert-sort"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Num 82))) ; theorem :: SCMISORT:33 (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 82))) "holds" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_scmisort :::"insert-sort"::: ) (Set (Var "f")) ")" ))))) ; theorem :: SCMISORT:34 (Bool "(" (Bool (Set ($#k2_scmisort :::"insert-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#v3_scm_halt :::"keepInt0_1"::: ) ) & (Bool (Set ($#k2_scmisort :::"insert-sort"::: ) (Set "(" ($#k5_scmfsa_2 :::"fsloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) "is" ($#v2_scm_halt :::"InitHalting"::: ) ) ")" ) ; theorem :: SCMISORT:35 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "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 "(" ($#k2_scmisort :::"insert-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 "(" ($#k2_scmisort :::"insert-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 "(" ($#k2_scmisort :::"insert-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 :: SCMISORT:36 (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 ($#k3_scmisort :::"Insert-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 ($#k3_scmisort :::"Insert-Sort-Algorithm"::: ) ))))))) ; theorem :: SCMISORT:37 (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"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "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 ($#k3_scmisort :::"Insert-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 :: SCMISORT:38 (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 ($#k3_scmisort :::"Insert-Sort-Algorithm"::: ) ) ($#v4_extpro_1 :::"-autonomic"::: ) )) ; registration cluster (Set ($#k3_scmisort :::"Insert-Sort-Algorithm"::: ) ) -> ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ; end; theorem :: SCMISORT:39 (Bool (Set ($#k3_scmisort :::"Insert-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"::: ) )) ;