:: SCMPDS_9  semantic presentation begin  














definitionlet "la", "lb" be   ($#m1_subset_1 :::"Int_position":::); let "a", "b" be   ($#m1_hidden :::"Integer":::); :: original: :::"-->"::: redefine func  "(" "la" "," "lb" ")"  :::"-->":::  "(" "a" "," "b" ")"  ->   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ); end; registrationlet "k" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k3_scmpds_2 :::"goto"::: )  "k" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMPDS_9:1 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("   "for" (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 (Var "l")))) "holds"  (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")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set (Var "i")) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMPDS_9:2 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set (Var "i")) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))  ")" )) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set (Var "i"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )) ; 
 
theorem :: SCMPDS_9:3 (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k3_scmpds_2 :::"goto"::: )  (Set (Var "k")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMPDS_9:4 (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 (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k4_scmpds_2 :::"return"::: )  (Set (Var "a")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))  "}"  ))) ; 
 
theorem :: SCMPDS_9:5 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k6_scmpds_2 :::"saveIC"::: )   "(" (Set (Var "a")) "," (Set (Var "k1")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:6 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "(" (Set (Var "a"))  ($#k5_scmpds_2 :::":="::: )  (Set (Var "k1")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:7 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k10_scmpds_2 :::":="::: )  (Set (Var "k2")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int_position":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k16_scmpds_2 :::":="::: )   "(" (Set (Var "b")) "," (Set (Var "k2")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:9 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k11_scmpds_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int_position":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k12_scmpds_2 :::"AddTo"::: )   "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int_position":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k13_scmpds_2 :::"SubFrom"::: )   "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int_position":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k14_scmpds_2 :::"MultBy"::: )   "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Int_position":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  ($#k15_scmpds_2 :::"Divide"::: )   "(" (Set (Var "a")) "," (Set (Var "k1")) "," (Set (Var "b")) "," (Set (Var "k2")) ")"  ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:14 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k7_scmpds_2 :::"<>0_goto"::: )  (Set (Var "k2")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) "," (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "k2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:15 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k8_scmpds_2 :::"<=0_goto"::: )  (Set (Var "k2")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) "," (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "k2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:16 (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"::: )  )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_amistd_1 :::"NIC"::: )   "(" (Set  "("  "(" (Set (Var "a")) "," (Set (Var "k1")) ")"   ($#k9_scmpds_2 :::">=0_goto"::: )  (Set (Var "k2")) ")" ) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "l")) ")" ) "," (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "k2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMPDS_9:17 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int_position":::) "holds"  (Bool (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k4_scmpds_2 :::"return"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))  "}"  )) ; 
 registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k4_scmpds_2 :::"return"::: )  "a" ")" )) ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); let "k1" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k6_scmpds_2 :::"saveIC"::: )   "(" "a" "," "k1" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); let "k1" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "(" "a"  ($#k5_scmpds_2 :::":="::: )  "k1" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  "(" "a" "," "k1" ")"   ($#k10_scmpds_2 :::":="::: )  "k2" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  "(" "a" "," "k1" ")"   ($#k16_scmpds_2 :::":="::: )   "(" "b" "," "k2" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k11_scmpds_2 :::"AddTo"::: )   "(" "a" "," "k1" "," "k2" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k12_scmpds_2 :::"AddTo"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k13_scmpds_2 :::"SubFrom"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k14_scmpds_2 :::"MultBy"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  ($#k15_scmpds_2 :::"Divide"::: )   "(" "a" "," "k1" "," "b" "," "k2" ")"  ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "a" be   ($#m1_subset_1 :::"Int_position":::); let "k1", "k2" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  "(" "a" "," "k1" ")"   ($#k7_scmpds_2 :::"<>0_goto"::: )  "k2" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  "(" "a" "," "k1" ")"   ($#k8_scmpds_2 :::"<=0_goto"::: )  "k2" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 

cluster (Set   ($#k2_amistd_1 :::"JUMP"::: )  (Set  "("  "(" "a" "," "k1" ")"   ($#k9_scmpds_2 :::">=0_goto"::: )  "k2" ")" )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMPDS_9:18 (Bool  "for" (Set (Var "l")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k3_amistd_1 :::"SUCC"::: )   "(" (Set (Var "l")) "," (Set  ($#k1_scmpds_2 :::"SCMPDS"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 registration
cluster (Set   ($#k1_scmpds_2 :::"SCMPDS"::: )  ) ->  ($#~v1_ami_wstd  "non"   ($#v1_ami_wstd :::"InsLoc-antisymmetric"::: )   )  ; 
end; registration
cluster (Set   ($#k1_scmpds_2 :::"SCMPDS"::: )  ) ->  ($#~v2_ami_wstd  "non"   ($#v2_ami_wstd :::"weakly_standard"::: )   )  ; 
end;