:: SCMPDS_4  semantic presentation begin  


































theorem :: SCMPDS_4:1 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "holds"  (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set  ($#k4_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 4) "," (Num 5) "," (Num 6) "," (Num 14) ($#k4_enumset1 :::"}"::: ) )) "or" (Bool (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s")) ")" )))  ")" ))) ; 
 
theorem :: SCMPDS_4:2 (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")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" )) "holds"  (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Var "s2")))) ; 
 
theorem :: SCMPDS_4:3 (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "k2")))) "holds"  (Bool (Set   ($#k2_scmpds_2 :::"DataLoc"::: )   "(" (Set (Var "k1")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_scmpds_2 :::"DataLoc"::: )   "(" (Set (Var "k2")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) ; 
 
theorem :: SCMPDS_4:4 (Bool  "for" (Set (Var "dl")) "being"   ($#m1_subset_1 :::"Int_position":::) (Bool  "ex" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "dl"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_scmpds_2 :::"DataLoc"::: )   "(" (Set (Var "i")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )))) ; 
 scheme  :: SCMPDS_4:sch 1 SCMPDSEx{ F1(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_hidden :::"Integer":::), F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) } : 
(Bool  "ex" (Set (Var "S")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "st"  (Bool  "("  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_scmpds_2 :::"DataLoc"::: )   "(" (Set (Var "i")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "i")) ")" ))  ")" )  ")" ))
 proof 


end; 
theorem :: SCMPDS_4:5 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )))) ; 
 
theorem :: SCMPDS_4:6 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "s")))) "or" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Int_position":::)) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"IC"::: )  ))  ")" ))) ; 
 
theorem :: SCMPDS_4:7 canceled; 
 
theorem :: SCMPDS_4:8 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" ) "iff" (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))  ")" )) ; 
 


begin  notationlet "I", "J" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); synonym "I" :::"';'"::: "J" for "I" :::"^"::: "J"; end; definitionlet "I", "J" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); :: original: :::"';'"::: redefine func "I" :::"';'"::: "J" ->   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_4:def 1 (Set "I"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k61_valued_1 :::"Shift"::: )   "(" "J" "," (Set  "("  ($#k5_card_1 :::"card"::: )  "I" ")" ) ")"  ")" )); end; 






:: deftheorem    defines :::"';'"::: SCMPDS_4:def 1 :  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set (Var "I"))  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "J")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" ) ")"  ")" )))); 
 begin  definitionlet "i" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "J" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func "i" :::"';'"::: "J" ->   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_4:def 2 (Set (Set  "("  ($#k9_compos_1 :::"Load"::: )  "i" ")" )  ($#k1_scmpds_4 :::"';'"::: )  "J"); end; 






:: deftheorem    defines :::"';'"::: SCMPDS_4:def 2 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set (Var "J")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_compos_1 :::"Load"::: )  (Set (Var "i")) ")" )  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "J")))))); 
 definitionlet "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "j" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func "I" :::"';'"::: "j" ->   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_4:def 3 (Set "I"  ($#k1_scmpds_4 :::"';'"::: )  (Set  "("  ($#k9_compos_1 :::"Load"::: )  "j" ")" )); end; 






:: deftheorem    defines :::"';'"::: SCMPDS_4:def 3 :  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_scmpds_4 :::"';'"::: )  (Set  "("  ($#k9_compos_1 :::"Load"::: )  (Set (Var "j")) ")" ))))); 
 definitionlet "i", "j" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func "i" :::"';'"::: "j" ->   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_4:def 4 (Set (Set  "("  ($#k9_compos_1 :::"Load"::: )  "i" ")" )  ($#k1_scmpds_4 :::"';'"::: )  (Set  "("  ($#k9_compos_1 :::"Load"::: )  "j" ")" )); end; 






:: deftheorem    defines :::"';'"::: SCMPDS_4:def 4 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_compos_1 :::"Load"::: )  (Set (Var "i")) ")" )  ($#k1_scmpds_4 :::"';'"::: )  (Set  "("  ($#k9_compos_1 :::"Load"::: )  (Set (Var "j")) ")" )))); 
 
theorem :: SCMPDS_4:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_compos_1 :::"Load"::: )  (Set (Var "i")) ")" )  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "j"))))) ; 
 
theorem :: SCMPDS_4:10 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set  "("  ($#k9_compos_1 :::"Load"::: )  (Set (Var "j")) ")" )))) ; 
 
theorem :: SCMPDS_4:11 (Bool  "for" (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "J")) ")" )  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "J"))  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMPDS_4:12 (Bool  "for" (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "I")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "j")) ")" )  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "j"))  ($#k2_scmpds_4 :::"';'"::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SCMPDS_4:13 (Bool  "for" (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "j")) ")" )  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "j"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMPDS_4:14 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "J")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set (Var "J")) ")" )  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "J"))  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SCMPDS_4:15 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set (Var "J")) ")" )  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "J"))  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMPDS_4:16 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "j")) ")" )  ($#k1_scmpds_4 :::"';'"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "j"))  ($#k2_scmpds_4 :::"';'"::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SCMPDS_4:17 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "j")) ")" )  ($#k3_scmpds_4 :::"';'"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k2_scmpds_4 :::"';'"::: )  (Set  "(" (Set (Var "j"))  ($#k4_scmpds_4 :::"';'"::: )  (Set (Var "k")) ")" )))) ; 
 





theorem :: SCMPDS_4:18 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_memstr_0 :::"Start-At"::: )   "(" (Set (Var "l")) "," (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")"  ")" )))))) ; 
 definitionlet "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "li" be   ($#m1_subset_1 :::"Int_position":::); let "k" be   ($#m1_hidden :::"Integer":::); :: original: :::"+*"::: redefine func "s" :::"+*":::  "(" "li" "," "k" ")"  ->   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); end; begin  definitionlet "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "P" be   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); func  :::"IExec":::  "(" "I" "," "P" "," "s" ")"  ->   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) equals :: SCMPDS_4:def 5 (Set   ($#k6_extpro_1 :::"Result"::: )   "(" (Set  "(" "P"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k10_compos_1 :::"stop"::: )  "I" ")" ) ")" ) "," "s" ")" ); end; 







:: deftheorem    defines :::"IExec"::: SCMPDS_4:def 5 :  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "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 "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"  (Bool (Set   ($#k6_scmpds_4 :::"IExec"::: )   "(" (Set (Var "I")) "," (Set (Var "P")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_extpro_1 :::"Result"::: )   "(" (Set  "(" (Set (Var "P"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k10_compos_1 :::"stop"::: )  (Set (Var "I")) ")" ) ")" ) "," (Set (Var "s")) ")" ))))); 
 definitionlet "I" be   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); attr "I" is  :::"paraclosed":::  means :: SCMPDS_4:def 6 (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 "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set   ($#k10_compos_1 :::"stop"::: )  "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 (Var "n")) ")"  ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set  "("  ($#k10_compos_1 :::"stop"::: )  "I" ")" )))))); attr "I" is  :::"parahalting":::  means :: SCMPDS_4:def 7 (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 "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set   ($#k10_compos_1 :::"stop"::: )  "I")  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "P"))  ($#r1_extpro_1 :::"halts_on"::: )  (Set (Var "s"))))); end; 








:: deftheorem    defines :::"paraclosed"::: SCMPDS_4:def 6 :  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "I")) "is"   ($#v1_scmpds_4 :::"paraclosed"::: )  ) "iff" (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 "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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 (Var "n")) ")"  ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set  "("  ($#k10_compos_1 :::"stop"::: )  (Set (Var "I")) ")" ))))))  ")" )); 
 
:: deftheorem    defines :::"parahalting"::: SCMPDS_4:def 7 :  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "I")) "is"   ($#v2_scmpds_4 :::"parahalting"::: )  ) "iff" (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 "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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 (Var "P"))  ($#r1_extpro_1 :::"halts_on"::: )  (Set (Var "s")))))  ")" )); 
 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"::: )     ($#v1_finset_1 :::"finite"::: )   bbbadV4_CARD_3() bbbadV1_AFINSQ_1() bbbadV2_PRE_POLY()   ($#v2_scmpds_4 :::"parahalting"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: SCMPDS_4:19 canceled; 
 
theorem :: SCMPDS_4:20 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set (Var "Q"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  "(" (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s")) ")" ) ")" ) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set  "("  ($#k3_scmpds_2 :::"goto"::: )  (Num 1) ")" ) "," (Set  "("  ($#k3_scmpds_2 :::"goto"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Num 1) ")" ) ")" ) ")"  ")" )))) "holds"  (Bool  "not" (Bool (Set (Var "Q"))  ($#r1_extpro_1 :::"halts_on"::: )  (Set (Var "s")))))) ; 
 
theorem :: SCMPDS_4:21 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Var "s2"))) & (Bool (Set (Var "I"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "I"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2"))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "m")) ")"  ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "I"))))  ")" )) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "m")) ")" ))))))) ; 
 







registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#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"::: )     ($#v1_finset_1 :::"finite"::: )   bbbadV1_AFINSQ_1()   ($#v2_scmpds_4 :::"parahalting"::: )    ->   ($#v1_scmpds_4 :::"paraclosed"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; begin  definitionlet "i" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "i" :::"valid_at"::: "n" means :: SCMPDS_4:def 8 (Bool  "("   "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_hidden :::"="::: )  (Num 14))) "implies" (Bool  "ex" (Set (Var "k1")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool "i"  ($#r1_hidden :::"="::: )  (Set   ($#k3_scmpds_2 :::"goto"::: )  (Set (Var "k1")))) & (Bool (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k1")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))  ")"  &  "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_hidden :::"="::: )  (Num 4))) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)(Bool  "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool "i"  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k7_scmpds_2 :::"<>0_goto"::: )  (Set (Var "k2")))) & (Bool (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")"  &  "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_hidden :::"="::: )  (Num 5))) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)(Bool  "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool "i"  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k8_scmpds_2 :::"<=0_goto"::: )  (Set (Var "k2")))) & (Bool (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")"  &  "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_hidden :::"="::: )  (Num 6))) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)(Bool  "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool "i"  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k9_scmpds_2 :::">=0_goto"::: )  (Set (Var "k2")))) & (Bool (Set "n"  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")"   ")" ); end; 





:: deftheorem    defines :::"valid_at"::: SCMPDS_4:def 8 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "i"))  ($#r1_scmpds_4 :::"valid_at"::: )  (Set (Var "n"))) "iff" (Bool  "("   "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 14))) "implies" (Bool  "ex" (Set (Var "k1")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_scmpds_2 :::"goto"::: )  (Set (Var "k1")))) & (Bool (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k1")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))  ")"  &  "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 4))) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)(Bool  "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k7_scmpds_2 :::"<>0_goto"::: )  (Set (Var "k2")))) & (Bool (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")"  &  "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 5))) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)(Bool  "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k8_scmpds_2 :::"<=0_goto"::: )  (Set (Var "k2")))) & (Bool (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")"  &  "("  (Bool (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 6))) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)(Bool  "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k9_scmpds_2 :::">=0_goto"::: )  (Set (Var "k2")))) & (Bool (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))  ")"   ")" )  ")" ))); 
 


definitionlet "IT" be (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"::: )    ($#m1_hidden :::"Function":::); attr "IT" is  :::"shiftable":::  means :: SCMPDS_4:def 9 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "IT")) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set "IT"  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 3)) & (Bool (Set (Var "i"))  ($#r1_scmpds_4 :::"valid_at"::: )  (Set (Var "n")))  ")" ))); end; 




:: deftheorem    defines :::"shiftable"::: SCMPDS_4:def 9 :  (Bool  "for" (Set (Var "IT")) "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"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_scmpds_4 :::"shiftable"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "IT")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "IT"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 3)) & (Bool (Set (Var "i"))  ($#r1_scmpds_4 :::"valid_at"::: )  (Set (Var "n")))  ")" )))  ")" )); 
 
theorem :: SCMPDS_4:22 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_scmpds_4 :::"valid_at"::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "i"))  ($#r1_scmpds_4 :::"valid_at"::: )  (Set (Var "n"))))) ; 
 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"::: )     ($#v1_finset_1 :::"finite"::: )   bbbadV4_CARD_3() bbbadV1_AFINSQ_1() bbbadV2_PRE_POLY()   ($#v2_scmpds_4 :::"parahalting"::: )     ($#v3_scmpds_4 :::"shiftable"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "i" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); attr "i" is  :::"shiftable":::  means :: SCMPDS_4:def 10 (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_hidden :::"<>"::: )  (Num 14)) & (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  "i")  ($#r1_xxreal_0 :::">"::: )  (Num 6))  ")" )  ")" ); end; 




:: deftheorem    defines :::"shiftable"::: SCMPDS_4:def 10 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "i")) "is"   ($#v4_scmpds_4 :::"shiftable"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Num 2)) "or" (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 14)) & (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::">"::: )  (Num 6))  ")" )  ")" )  ")" )); 
 registration
cluster   ($#v4_scmpds_4 :::"shiftable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "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") ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set  "(" "a" "," "k1" ")"   ($#k10_scmpds_2 :::":="::: )  "k2") ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 
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" ")" ) ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 
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" ")" ) ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 

cluster (Set   ($#k13_scmpds_2 :::"SubFrom"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")" ) ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 

cluster (Set   ($#k14_scmpds_2 :::"MultBy"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")" ) ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 

cluster (Set   ($#k15_scmpds_2 :::"Divide"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")" ) ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 

cluster (Set  "(" "a" "," "k1" ")"   ($#k16_scmpds_2 :::":="::: )   "(" "b" "," "k2" ")" ) ->   ($#v4_scmpds_4 :::"shiftable"::: )   ; 
end; registrationlet "I", "J" be   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
cluster (Set "I"  ($#k1_ordinal4 :::"';'"::: )  "J") ->   ($#v3_scmpds_4 :::"shiftable"::: )    for  ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
end; registrationlet "i" be   ($#v4_scmpds_4 :::"shiftable"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
cluster (Set   ($#k3_afinsq_1 :::"Load"::: )  ) ->   ($#v3_scmpds_4 :::"shiftable"::: )    for  ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
end; registrationlet "i" be   ($#v4_scmpds_4 :::"shiftable"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "J" be   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
cluster (Set "i"  ($#k2_scmpds_4 :::"';'"::: )  "J") ->   ($#v3_scmpds_4 :::"shiftable"::: )   ; 
end; registrationlet "I" be   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); let "j" be   ($#v4_scmpds_4 :::"shiftable"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
cluster (Set "I"  ($#k3_scmpds_4 :::"';'"::: )  "j") ->   ($#v3_scmpds_4 :::"shiftable"::: )   ; 
end; registrationlet "i", "j" be   ($#v4_scmpds_4 :::"shiftable"::: )    ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
cluster (Set "i"  ($#k4_scmpds_4 :::"';'"::: )  "j") ->   ($#v3_scmpds_4 :::"shiftable"::: )   ; 
end; registration
cluster (Set   ($#k4_compos_1 :::"Stop"::: )  (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )) ->   ($#v2_scmpds_4 :::"parahalting"::: )     ($#v3_scmpds_4 :::"shiftable"::: )   ; 
end; registrationlet "I" be   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
cluster (Set   ($#k10_compos_1 :::"stop"::: )  "I") ->   ($#v3_scmpds_4 :::"shiftable"::: )   ; 
end; 
theorem :: SCMPDS_4:23 (Bool  "for" (Set (Var "I")) "being"   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k1")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set  "("  ($#k3_scmpds_2 :::"goto"::: )  (Set (Var "k1")) ")" )) "is"   ($#v3_scmpds_4 :::"shiftable"::: )  ))) ; 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k3_afinsq_1 :::"Load"::: )  ) ->   ($#v3_scmpds_4 :::"shiftable"::: )    for  ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
end; 
theorem :: SCMPDS_4:24 (Bool  "for" (Set (Var "I")) "being"   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)  "st" (Bool (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k7_scmpds_2 :::"<>0_goto"::: )  (Set (Var "k2")) ")" )) "is"   ($#v3_scmpds_4 :::"shiftable"::: )  )))) ; 
 registrationlet "k1" be   ($#m1_hidden :::"Integer":::); let "a" be   ($#m1_subset_1 :::"Int_position":::); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k3_afinsq_1 :::"Load"::: )  ) ->   ($#v3_scmpds_4 :::"shiftable"::: )    for  ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
end; 
theorem :: SCMPDS_4:25 (Bool  "for" (Set (Var "I")) "being"   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)  "st" (Bool (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k8_scmpds_2 :::"<=0_goto"::: )  (Set (Var "k2")) ")" )) "is"   ($#v3_scmpds_4 :::"shiftable"::: )  )))) ; 
 registrationlet "k1" be   ($#m1_hidden :::"Integer":::); let "a" be   ($#m1_subset_1 :::"Int_position":::); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k3_afinsq_1 :::"Load"::: )  ) ->   ($#v3_scmpds_4 :::"shiftable"::: )    for  ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
end; 
theorem :: SCMPDS_4:26 (Bool  "for" (Set (Var "I")) "being"   ($#v3_scmpds_4 :::"shiftable"::: )    ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::)  "st" (Bool (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "I"))  ($#k3_scmpds_4 :::"';'"::: )  (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k9_scmpds_2 :::">=0_goto"::: )  (Set (Var "k2")) ")" )) "is"   ($#v3_scmpds_4 :::"shiftable"::: )  )))) ; 
 registrationlet "k1" be   ($#m1_hidden :::"Integer":::); let "a" be   ($#m1_subset_1 :::"Int_position":::); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k3_afinsq_1 :::"Load"::: )  ) ->   ($#v3_scmpds_4 :::"shiftable"::: )    for  ($#m1_hidden :::"Program":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); 
end; 
theorem :: SCMPDS_4:27 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k1")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s2"))))) "holds"  (Bool (Set (Set  "("  ($#k17_scmpds_2 :::"ICplusConst"::: )   "(" (Set (Var "s1")) "," (Set (Var "k1")) ")"  ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k17_scmpds_2 :::"ICplusConst"::: )   "(" (Set (Var "s2")) "," (Set (Var "k1")) ")" ))))) ; 
 
theorem :: SCMPDS_4:28 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Var "i"))  ($#r1_scmpds_4 :::"valid_at"::: )  (Set (Var "m"))) & (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Num 3)) & (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s2")))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s1")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s2")) ")"  ")" ))) & (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_4:29 (Bool  "for" (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "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 "P1")))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set  "("  ($#k10_compos_1 :::"stop"::: )  (Set (Var "J")) ")" ) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "P2"))) & (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" ))) & (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   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P2")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" ) ")" )) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )))  ")" ))))))) ;