:: SCMFSA_M  semantic presentation begin  
















registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  "n" ")" )  ($#k16_funcop_1 :::".-->"::: )  "i") -> (Set   ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_funct_1 :::"-compatible"::: )   ; 
end; definitionlet "I" be   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func  :::"Initialized"::: "I" ->   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA_M:def 1 (Set "I"  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" )); projectivity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b2"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b1"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" ))))
 ; end; 





:: deftheorem    defines :::"Initialized"::: SCMFSA_M:def 1 :  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" )))); 
 registrationlet "I" be   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set   ($#k1_scmfsa_m :::"Initialized"::: )  "I") -> (Set   ($#k6_numbers :::"0"::: )  )  ($#v5_memstr_0 :::"-started"::: )   ; 
end; registrationlet "I" be   ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set   ($#k1_scmfsa_m :::"Initialized"::: )  "I") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; scheme  :: SCMFSA_M:sch 1 SCMFSAEx{ F1(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_hidden :::"Integer":::), F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ), F3() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) } : 
(Bool  "ex" (Set (Var "S")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st"  (Bool  "("  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "i")) ")" )) & (Bool (Set (Set (Var "S"))  ($#k18_scmfsa_2 :::"."::: )  (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "i")) ")" ))  ")" )  ")" )  ")" ))
 proof 


end; 
theorem :: SCMFSA_M:1 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (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-Location":::)) "or" (Bool (Set (Var "x")) "is"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"IC"::: )  ))  ")" ))) ; 
 
theorem :: SCMFSA_M:2 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set (Var "s1"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))  ")" )  ")" ) "iff" (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))  ")" )) ; 
 
theorem :: SCMFSA_M:3 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; 
 registrationlet "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set   ($#k1_scmfsa_m :::"Initialized"::: )  "s") ->   ($#v1_partfun1 :::"total"::: )   ; 
end; 
theorem :: SCMFSA_M:4 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" )))) ; 
 
theorem :: SCMFSA_M:5 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: SCMFSA_M:6 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")))))) "holds"  (Bool  "not" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" )))))) ; 
 
theorem :: SCMFSA_M:7 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")))))) "holds"  (Bool  "not" (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" )))))) ; 
 
theorem :: SCMFSA_M:8 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) ; 
 
theorem :: SCMFSA_M:9 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: SCMFSA_M:10 (Bool (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" ))) ; 
 
theorem :: SCMFSA_M:11 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ) ($#k7_domain_1 :::"}"::: ) )) ; 
 
theorem :: SCMFSA_M:12 (Bool (Set (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: SCMFSA_M:13 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "p"))))) ; 
 begin  registration
cluster (Set   ($#k2_scm_inst :::"Int-Locations"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "IT" be   ($#m1_subset_1 :::"Int-Location":::); attr "IT" is  :::"read-only":::  means :: SCMFSA_M:def 2 (Bool "IT"  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ))); end; 




:: deftheorem    defines :::"read-only"::: SCMFSA_M:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_scmfsa_m :::"read-only"::: )  ) "iff" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )); 
 notationlet "IT" be   ($#m1_subset_1 :::"Int-Location":::); antonym  :::"read-write"::: "IT" for  :::"read-only"::: ; end; registration
cluster (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) )) ->   ($#v1_scmfsa_m :::"read-only"::: )   ; 
end; registration
cluster   ($#v1_ami_2 :::"Int-like"::: )     ($#v1_scmfsa_m :::"read-write"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )); 
end; 


definitionlet "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); func  :::"FirstNotIn"::: "L" ->   ($#m1_subset_1 :::"Int-Location":::) means :: SCMFSA_M:def 3 (Bool  "ex" (Set (Var "sn")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set (Var "sn")) ")" ))) & (Bool (Set (Var "sn"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Bool  "not" (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  "L"))  "}"  )  ")" )); end; 





:: deftheorem    defines :::"FirstNotIn"::: SCMFSA_M:def 3 :  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_scmfsa_m :::"FirstNotIn"::: )  (Set (Var "L")))) "iff" (Bool  "ex" (Set (Var "sn")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set (Var "sn")) ")" ))) & (Bool (Set (Var "sn"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Bool  "not" (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))  "}"  )  ")" ))  ")" ))); 
 
theorem :: SCMFSA_M:14 (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  "holds" (Bool (Bool  "not" (Set   ($#k2_scmfsa_m :::"FirstNotIn"::: )  (Set (Var "L")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))) ; 
 
theorem :: SCMFSA_M:15 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  "st" (Bool (Bool (Set   ($#k2_scmfsa_m :::"FirstNotIn"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "m")))) & (Bool (Bool  "not" (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))))) ; 
 


definitionlet "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ); func  :::"First*NotIn"::: "L" ->    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   means :: SCMFSA_M:def 4 (Bool  "ex" (Set (Var "sn")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set (Var "sn")) ")" ))) & (Bool (Set (Var "sn"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Bool  "not" (Set   ($#k5_scmfsa_2 :::"fsloc"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  "L"))  "}"  )  ")" )); end; 





:: deftheorem    defines :::"First*NotIn"::: SCMFSA_M:def 4 :  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) )  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_scmfsa_m :::"First*NotIn"::: )  (Set (Var "L")))) "iff" (Bool  "ex" (Set (Var "sn")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set (Var "sn")) ")" ))) & (Bool (Set (Var "sn"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Bool  "not" (Set   ($#k5_scmfsa_2 :::"fsloc"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))  "}"  )  ")" ))  ")" ))); 
 
theorem :: SCMFSA_M:16 (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) )  "holds" (Bool (Bool  "not" (Set   ($#k3_scmfsa_m :::"First*NotIn"::: )  (Set (Var "L")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))) ; 
 
theorem :: SCMFSA_M:17 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) )  "st" (Bool (Bool (Set   ($#k3_scmfsa_m :::"First*NotIn"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmfsa_2 :::"fsloc"::: )  (Set (Var "m")))) & (Bool (Bool  "not" (Set   ($#k5_scmfsa_2 :::"fsloc"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))))) ; 
 registrationlet "s" be   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "li" be   ($#m1_subset_1 :::"Int-Location":::); let "k" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "s"  ($#k2_funct_7 :::"+*"::: )   "(" "li" "," "k" ")" ) -> (Set   ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_funct_1 :::"-compatible"::: )   ; 
end; begin  registrationlet "a" be   ($#m1_subset_1 :::"Int-Location":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "a"  ($#k16_funcop_1 :::".-->"::: )  "n") ->   ($#v4_memstr_0 :::"data-only"::: )    for  ($#m1_hidden :::"PartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
end; 
theorem :: SCMFSA_M:18 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k8_memstr_0 :::"Initialize"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s"))))) ; 
 
theorem :: SCMFSA_M:19 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s"))))) ; 
 
theorem :: SCMFSA_M:20 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set (Var "s1"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))  ")" )) "holds"  (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) ; 
 
theorem :: SCMFSA_M:21 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k7_memstr_0 :::"Start-At"::: )   "(" (Set (Var "l")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))))) ; 
 begin  definitionlet "d" be   ($#m1_subset_1 :::"Int-Location":::); :: original: :::"{"::: redefine func :::"{":::"d":::"}"::: ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); let "e" be   ($#m1_subset_1 :::"Int-Location":::); :: original: :::"{"::: redefine func :::"{":::"d" "," "e":::"}"::: ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); let "f" be   ($#m1_subset_1 :::"Int-Location":::); :: original: :::"{"::: redefine func :::"{":::"d" "," "e" "," "f":::"}"::: ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); let "g" be   ($#m1_subset_1 :::"Int-Location":::); :: original: :::"{"::: redefine func :::"{":::"d" "," "e" "," "f" "," "g":::"}"::: ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); end; definitionlet "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); func  :::"RWNotIn-seq"::: "L" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ) ")" ) means :: SCMFSA_M:def 5 (Bool  "("  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Bool  "not" (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  "L")) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "sn")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "sn")))) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "sn"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set (Var "sn")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "is"   ($#v1_finset_1 :::"infinite"::: )  )  ")" )  ")" ); end; 





:: deftheorem    defines :::"RWNotIn-seq"::: SCMFSA_M:def 5 :  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Bool  "not" (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "L")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  "}"  ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "sn")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "sn")))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "sn"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set (Var "sn")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i"))) "is"   ($#v1_finset_1 :::"infinite"::: )  )  ")" )  ")" )  ")" ))); 
 registrationlet "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); let "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  "L" ")" )  ($#k1_funct_1 :::"."::: )  "n") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 



theorem :: SCMFSA_M:22 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) "holds"   (Bool  "("  (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "n"))))) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "not" (Bool (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))))  ")" )  ")" ))) ; 
 
theorem :: SCMFSA_M:23 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  "holds" (Bool (Set   ($#k6_seq_4 :::"min"::: )  (Set  "(" (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_seq_4 :::"min"::: )  (Set  "(" (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: SCMFSA_M:24 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k6_seq_4 :::"min"::: )  (Set  "(" (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_seq_4 :::"min"::: )  (Set  "(" (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "m")) ")" ))))) ; 
 definitionlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); func "n" :::"-thRWNotIn"::: "L" ->   ($#m1_subset_1 :::"Int-Location":::) equals :: SCMFSA_M:def 6 (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set  "(" (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  "L" ")" )  ($#k3_funct_2 :::"."::: )  "n" ")" ) ")" )); end; 






:: deftheorem    defines :::"-thRWNotIn"::: SCMFSA_M:def 6 :  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) "holds"  (Bool (Set (Set (Var "n"))  ($#k9_scmfsa_m :::"-thRWNotIn"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  "("  ($#k6_seq_4 :::"min"::: )  (Set  "(" (Set  "("  ($#k8_scmfsa_m :::"RWNotIn-seq"::: )  (Set (Var "L")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))); 
 notationlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); synonym "n" :::"-stRWNotIn"::: "L" for "n" :::"-thRWNotIn"::: "L"; synonym "n" :::"-ndRWNotIn"::: "L" for "n" :::"-thRWNotIn"::: "L"; synonym "n" :::"-rdRWNotIn"::: "L" for "n" :::"-thRWNotIn"::: "L"; end; registrationlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "L" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ); 
cluster (Set "n"  ($#k9_scmfsa_m :::"-thRWNotIn"::: )  "L") ->   ($#v1_scmfsa_m :::"read-write"::: )   ; 
end; 
theorem :: SCMFSA_M:25 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  "holds" (Bool (Bool  "not" (Set (Set (Var "n"))  ($#k9_scmfsa_m :::"-thRWNotIn"::: )  (Set (Var "L")))  ($#r2_hidden :::"in"::: )  (Set (Var "L")))))) ; 
 
theorem :: SCMFSA_M:26 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "L")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k9_scmfsa_m :::"-thRWNotIn"::: )  (Set (Var "L")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "m"))  ($#k9_scmfsa_m :::"-thRWNotIn"::: )  (Set (Var "L")))))) ; 
 begin  
theorem :: SCMFSA_M:27 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "Iloc")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) )  (Bool  "for" (Set (Var "Floc")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "s1"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "Iloc"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Floc")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "Iloc"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Floc")) ")" ))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Iloc")))) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Floc")))) "holds"  (Bool (Set (Set (Var "s1"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "x"))))  ")" )  ")" )  ")" )))) ; 
 
theorem :: SCMFSA_M:28 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "Iloc")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "s1"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "Iloc"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "Iloc"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Iloc")))) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set (Var "s1"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s2"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "x"))))  ")" )  ")" )  ")" ))) ; 
 begin  
theorem :: SCMFSA_M:29 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "i")) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "m")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k7_memstr_0 :::"Start-At"::: )   "(" (Set (Var "n")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")"  ")" ) ")" ))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set (Var "i")))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"IC"::: )  ))  ")" ))) ; 
 
theorem :: SCMFSA_M:30 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set   ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "s")))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 registrationlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k4_scmfsa_2 :::"intloc"::: )  (Set  "(" "n"  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )) ->   ($#v1_scmfsa_m :::"read-write"::: )   ; 
end; begin  registrationlet "f" be    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )  ; let "t" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ); 
cluster (Set "f"  ($#k16_funcop_1 :::".-->"::: )  "t") -> (Set   ($#k2_memstr_0 :::"the_Values_of"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_funct_1 :::"-compatible"::: )   ; 
end; 
theorem :: SCMFSA_M:31 (Bool  "for" (Set (Var "w")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set  "(" (Set (Var "f"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "w")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k8_domain_1 :::"{"::: ) (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ) "," (Set (Var "f")) ($#k8_domain_1 :::"}"::: ) )))) ; 
 
theorem :: SCMFSA_M:32 (Bool  "for" (Set (Var "t")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k8_memstr_0 :::"Initialize"::: )  (Set  "(" (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Num 1) ")" ) ")" ))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "t")) ")" ))))) ; 
 
theorem :: SCMFSA_M:33 (Bool  "for" (Set (Var "w")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set   ($#k1_scmfsa_m :::"Initialized"::: )  (Set  "(" (Set (Var "f"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "w")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "s")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "w"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_scmfsa_2 :::"intloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )))) ; 
 
theorem :: SCMFSA_M:34 (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ) "," (Set (Var "f")) ($#k8_domain_1 :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "s"))))))) ; 
 definitionfunc  :::"Sorting-Function":::  ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) means :: SCMFSA_M:def 7 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "t")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )(Bool  "ex" (Set (Var "u")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "t")) "," (Set (Var "u"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) & (Bool (Set (Var "u")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )) & (Bool (Set (Var "u")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "t")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "u"))))  ")" )))  ")" )); end; 




:: deftheorem    defines :::"Sorting-Function"::: SCMFSA_M:def 7 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_scmfsa_m :::"Sorting-Function"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "ex" (Set (Var "t")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )(Bool  "ex" (Set (Var "u")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "t")) "," (Set (Var "u"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) & (Bool (Set (Var "u")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )) & (Bool (Set (Var "u")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "t")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "u"))))  ")" )))  ")" ))  ")" )); 
 
theorem :: SCMFSA_M:35 (Bool  "for" (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k10_scmfsa_m :::"Sorting-Function"::: ) ))) "iff" (Bool  "ex" (Set (Var "t")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "t")))))  ")" )) ; 
 
theorem :: SCMFSA_M:36 (Bool  "for" (Set (Var "t")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) (Bool  "ex" (Set (Var "u")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "t")) "," (Set (Var "u"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) & (Bool (Set (Var "u")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ) & (Bool (Set (Var "u")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )) & (Bool (Set (Set  ($#k10_scmfsa_m :::"Sorting-Function"::: ) )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmfsa_2 :::"fsloc"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "u"))))  ")" ))) ; 
 
theorem :: SCMFSA_M:37 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"   ($#v1_scmfsa_m :::"read-write"::: )    ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set  "("  ($#k1_scmfsa_m :::"Initialized"::: )  (Set (Var "s")) ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f"))))  ")" )  ")" )) ;