:: SCMPDS_3 semantic presentation begin theorem :: SCMPDS_3:1 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2"))))) "holds" (Bool (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s1")) "," (Set (Var "k1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s2")) "," (Set (Var "k1")) ")" )))) ; theorem :: SCMPDS_3:2 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )))))) ; theorem :: SCMPDS_3:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))) ; theorem :: SCMPDS_3:4 (Bool (Bool "not" (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ))) ; begin theorem :: SCMPDS_3:5 canceled; theorem :: SCMPDS_3:6 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "iloc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "iloc")) "," (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))) ; theorem :: SCMPDS_3:7 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "t")) ($#k5_relat_1 :::"|"::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ")" )) "is" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))) ; begin definitionlet "la" be ($#m1_subset_1 :::"Int_position":::); let "a" be ($#m1_hidden :::"Integer":::); :: original: :::".-->"::: redefine func "la" :::".-->"::: "a" -> ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); end; registration cluster (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) -> ($#v3_amistd_5 :::"IC-recognized"::: ) ; end; theorem :: SCMPDS_3:8 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool (Set (Var "k1")) ($#r1_hidden :::"<>"::: ) (Set (Var "k2"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1")))) & (Bool (Set (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k1"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k2"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s1")) "," (Set (Var "k1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s2")) "," (Set (Var "k2")) ")" )))) ; theorem :: SCMPDS_3:9 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool (Set (Var "k1")) ($#r1_hidden :::"<>"::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s1")) "," (Set (Var "k1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s2")) "," (Set (Var "k2")) ")" )))) ; theorem :: SCMPDS_3:10 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_scmpds_2 :::"ICplusConst"::: ) "(" (Set (Var "s")) "," (Num 1) ")" ))) ; registration cluster (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) -> ($#v4_amistd_5 :::"CurIns-recognized"::: ) ; end; theorem :: SCMPDS_3:11 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k16_scmpds_2 :::":="::: ) "(" (Set (Var "b")) "," (Set (Var "k2")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )))))))))) ; theorem :: SCMPDS_3:12 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )))))))))) ; theorem :: SCMPDS_3:13 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" )))))))))) ; theorem :: SCMPDS_3:14 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int_position":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")" )) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ) "," (Set (Var "k2")) ")" ")" ) ")" )))))))))) ; theorem :: SCMPDS_3:15 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) (Set (Var "k2")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k2"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "k2")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))))))) ; theorem :: SCMPDS_3:16 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) (Set (Var "k2")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k2"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "k2")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))))))) ; theorem :: SCMPDS_3:17 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b3")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "k1")) ")" ($#k9_scmpds_2 :::">=0_goto"::: ) (Set (Var "k2")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k2"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "k2")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_scmpds_2 :::"DataLoc"::: ) "(" (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set (Var "k1")) ")" ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))))))) ;