:: SCMPDS_5 semantic presentation begin theorem :: SCMPDS_5:1 canceled; theorem :: SCMPDS_5:2 canceled; theorem :: SCMPDS_5:3 canceled; theorem :: SCMPDS_5:4 canceled; theorem :: SCMPDS_5:5 canceled; theorem :: SCMPDS_5:6 canceled; theorem :: SCMPDS_5:7 canceled; theorem :: SCMPDS_5:8 canceled; theorem :: SCMPDS_5:9 canceled; theorem :: SCMPDS_5:10 canceled; theorem :: SCMPDS_5:11 canceled; theorem :: SCMPDS_5:12 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" )))) ; theorem :: SCMPDS_5:13 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" )))) ; theorem :: SCMPDS_5:14 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" )))) ; theorem :: SCMPDS_5:15 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))) ; theorem :: SCMPDS_5:16 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (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")) ")" ) ($#r1_hidden :::"="::: ) (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 :: SCMPDS_5:17 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set ($#k10_compos_1 :::"stop"::: ) (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")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P2")) "," (Set (Var "s")) ")" )) ")" )))) ; theorem :: SCMPDS_5:18 canceled; theorem :: SCMPDS_5:19 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "m")) ")" ))))))) ; theorem :: SCMPDS_5:20 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "m")) ")" ))))))) ; begin definitioncanceled; let "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); attr "i" is :::"parahalting"::: means :: SCMPDS_5:def 2 (Bool (Set ($#k9_compos_1 :::"Load"::: ) "i") "is" ($#v2_scmpds_4 :::"parahalting"::: ) ); end; :: deftheorem SCMPDS_5:def 1 : canceled; :: deftheorem defines :::"parahalting"::: SCMPDS_5:def 2 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#v1_scmpds_5 :::"parahalting"::: ) ) "iff" (Bool (Set ($#k9_compos_1 :::"Load"::: ) (Set (Var "i"))) "is" ($#v2_scmpds_4 :::"parahalting"::: ) ) ")" )); registration cluster ($#v6_compos_0 :::"No-StopCode"::: ) ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )); end; theorem :: SCMPDS_5:21 (Bool "for" (Set (Var "k1")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k3_scmpds_2 :::"goto"::: ) (Set (Var "k1"))) "is" ($#v6_compos_0 :::"No-StopCode"::: ) )) ; registrationlet "a" be ($#m1_subset_1 :::"Int_position":::); cluster (Set ($#k4_scmpds_2 :::"return"::: ) "a") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set "a" ($#k5_scmpds_2 :::":="::: ) "k1") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set ($#k6_scmpds_2 :::"saveIC"::: ) "(" "a" "," "k1" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); cluster (Set "(" "a" "," "k1" ")" ($#k7_scmpds_2 :::"<>0_goto"::: ) "k2") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set "(" "a" "," "k1" ")" ($#k8_scmpds_2 :::"<=0_goto"::: ) "k2") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set "(" "a" "," "k1" ")" ($#k9_scmpds_2 :::">=0_goto"::: ) "k2") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set "(" "a" "," "k1" ")" ($#k10_scmpds_2 :::":="::: ) "k2") -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" "a" "," "k1" "," "k2" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set ($#k15_scmpds_2 :::"Divide"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; cluster (Set "(" "a" "," "k1" ")" ($#k16_scmpds_2 :::":="::: ) "(" "b" "," "k2" ")" ) -> ($#v6_compos_0 :::"No-StopCode"::: ) ; end; registration cluster (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) )) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; end; registrationlet "i" be ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set ($#k3_afinsq_1 :::"Load"::: ) ) -> ($#v2_scmpds_4 :::"parahalting"::: ) for ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); end; registrationlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1" be ($#m1_hidden :::"Integer":::); cluster (Set "a" ($#k5_scmpds_2 :::":="::: ) "k1") -> ($#v1_scmpds_5 :::"parahalting"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); cluster (Set "(" "a" "," "k1" ")" ($#k10_scmpds_2 :::":="::: ) "k2") -> ($#v1_scmpds_5 :::"parahalting"::: ) ; cluster (Set ($#k11_scmpds_2 :::"AddTo"::: ) "(" "a" "," "k1" "," "k2" ")" ) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k12_scmpds_2 :::"AddTo"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; cluster (Set ($#k13_scmpds_2 :::"SubFrom"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; cluster (Set ($#k14_scmpds_2 :::"MultBy"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; cluster (Set ($#k15_scmpds_2 :::"Divide"::: ) "(" "a" "," "k1" "," "b" "," "k2" ")" ) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; cluster (Set "(" "a" "," "k1" ")" ($#k16_scmpds_2 :::":="::: ) "(" "b" "," "k2" ")" ) -> ($#v1_scmpds_5 :::"parahalting"::: ) ; end; theorem :: SCMPDS_5:22 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "not" (Bool (Set (Var "i")) "is" ($#v1_scmpds_5 :::"parahalting"::: ) ))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_relat_1 :::"Relation-like"::: ) (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_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() bbbadV1_AFINSQ_1() ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I", "J" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "I" ($#k1_ordinal4 :::"';'"::: ) "J") -> ($#v2_compos_1 :::"halt-free"::: ) ; end; registrationlet "i" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set ($#k3_afinsq_1 :::"Load"::: ) ) -> ($#v2_compos_1 :::"halt-free"::: ) ; end; registrationlet "i" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "J" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "i" ($#k2_scmpds_4 :::"';'"::: ) "J") -> ($#v2_compos_1 :::"halt-free"::: ) ; end; registrationlet "I" be ($#v2_compos_1 :::"halt-free"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "j" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "I" ($#k3_scmpds_4 :::"';'"::: ) "j") -> ($#v2_compos_1 :::"halt-free"::: ) ; end; registrationlet "i", "j" be ($#v6_compos_0 :::"No-StopCode"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "i" ($#k4_scmpds_4 :::"';'"::: ) "j") -> ($#v2_compos_1 :::"halt-free"::: ) ; end; theorem :: SCMPDS_5:23 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "I"))) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: SCMPDS_5:24 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "I")))))))) ; theorem :: SCMPDS_5:25 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" )))))) ; theorem :: SCMPDS_5:26 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I"))))))) ; theorem :: SCMPDS_5:27 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) "or" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))) "or" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "I")))) ")" )))) ; theorem :: SCMPDS_5:28 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ))))))) ; theorem :: SCMPDS_5:29 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))))) ; theorem :: SCMPDS_5:30 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))))) ; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "J" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "I" ($#k1_ordinal4 :::"';'"::: ) "J") -> ($#v2_scmpds_4 :::"parahalting"::: ) for ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); end; registrationlet "i" be ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "J" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "i" ($#k2_scmpds_4 :::"';'"::: ) "J") -> ($#v2_scmpds_4 :::"parahalting"::: ) ; end; registrationlet "I" be ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "j" be ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "I" ($#k3_scmpds_4 :::"';'"::: ) "j") -> ($#v2_scmpds_4 :::"parahalting"::: ) ; end; registrationlet "i" be ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "j" be ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ); cluster (Set "i" ($#k4_scmpds_4 :::"';'"::: ) "j") -> ($#v2_scmpds_4 :::"parahalting"::: ) ; end; theorem :: SCMPDS_5:31 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "P1")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s1")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set (Var "J"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P1")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set (Var "s1")) "," (Set (Var "m")) ")" ))) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k4_extpro_1 :::"Following"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "n")) ")" ))))))) ; begin theorem :: SCMPDS_5:32 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set (Var "s")) "," (Set "(" (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ))))))) ; theorem :: SCMPDS_5:33 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) ")" ) ")" ) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "J")) ")" ) ")" ) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set "(" (Set (Var "P")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k10_compos_1 :::"stop"::: ) (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ))))))) ; theorem :: SCMPDS_5:34 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_memstr_0 :::"IncIC"::: ) "(" (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "I")) ")" ) ")" )))))) ; theorem :: SCMPDS_5:35 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "J")) "being" ($#v2_scmpds_4 :::"parahalting"::: ) ($#v3_scmpds_4 :::"shiftable"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_scmpds_4 :::"';'"::: ) (Set (Var "J")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "J")) "," (Set (Var "P")) "," (Set "(" ($#k8_memstr_0 :::"Initialize"::: ) (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; begin theorem :: SCMPDS_5:36 canceled; theorem :: SCMPDS_5:37 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st" (Bool (Bool (Set (Set (Var "s1")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" ) ($#k1_tarski :::"}"::: ) ) ")" )))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))) ; theorem :: SCMPDS_5:38 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "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 ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set (Var "s2")))) & (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Num 3))) "holds" (Bool (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s2")) ")" ")" ))))) ; theorem :: SCMPDS_5:39 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v4_scmpds_4 :::"shiftable"::: ) ($#m1_subset_1 :::"Instruction":::) "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 ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_memstr_0 :::"DataPart"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s2")) ")" ")" ))))) ; theorem :: SCMPDS_5:40 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" ($#k9_compos_1 :::"Load"::: ) (Set (Var "i")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ))))) ; theorem :: SCMPDS_5:41 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#v2_compos_1 :::"halt-free"::: ) ($#v2_scmpds_4 :::"parahalting"::: ) ($#m1_hidden :::"Program":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "I")) ($#k3_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SCMPDS_5:42 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int_position":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#v6_compos_0 :::"No-StopCode"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#v4_scmpds_4 :::"shiftable"::: ) ($#v1_scmpds_5 :::"parahalting"::: ) ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmpds_4 :::"IExec"::: ) "(" (Set "(" (Set (Var "i")) ($#k4_scmpds_4 :::"';'"::: ) (Set (Var "j")) ")" ) "," (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "j")) "," (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ;