:: SCMFSA_3  semantic presentation begin  
theorem :: SCMFSA_3:1 canceled; 
 
theorem :: SCMFSA_3:2 canceled; 
 










theorem :: SCMFSA_3:3 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "iloc")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Int-Location":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k7_memstr_0 :::"Start-At"::: )   "(" (Set (Var "iloc")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))))) ; 
 
theorem :: SCMFSA_3:4 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "iloc")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )   "holds"  (Bool (Set (Set (Var "s"))  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k7_memstr_0 :::"Start-At"::: )   "(" (Set (Var "iloc")) "," (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")"  ")" ) ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "a"))))))) ; 
 begin  definitionlet "la" be   ($#m1_subset_1 :::"Int-Location":::); let "a" be   ($#m1_hidden :::"Integer":::); :: original: :::".-->"::: redefine func "la" :::".-->"::: "a" ->   ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); end; registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v3_amistd_5 :::"IC-recognized"::: )   ; 
end; registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v4_amistd_5 :::"CurIns-recognized"::: )   ; 
end; 
theorem :: SCMFSA_3:5 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "da"))  ($#k6_scmfsa_2 :::":="::: )  (Set (Var "db")))) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")))))))))) ; 
 
theorem :: SCMFSA_3:6 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_scmfsa_2 :::"AddTo"::: )   "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))))))))) ; 
 
theorem :: SCMFSA_3:7 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmfsa_2 :::"SubFrom"::: )   "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))))))))) ; 
 
theorem :: SCMFSA_3:8 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_scmfsa_2 :::"MultBy"::: )   "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))))))))) ; 
 
theorem :: SCMFSA_3:9 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "da"))  ($#r1_hidden :::"<>"::: )  (Set (Var "db")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k5_int_1 :::"div"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k5_int_1 :::"div"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))))))))) ; 
 
theorem :: SCMFSA_3:10 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k10_scmfsa_2 :::"Divide"::: )   "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "db"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k6_int_1 :::"mod"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )  ($#k6_int_1 :::"mod"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))))))))) ; 
 
theorem :: SCMFSA_3:11 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "loc")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "da"))  ($#k12_scmfsa_2 :::"=0_goto"::: )  (Set (Var "loc")))) & (Bool (Set (Var "loc"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))))))) ; 
 
theorem :: SCMFSA_3:12 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "loc")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "da"))  ($#k13_scmfsa_2 :::">0_goto"::: )  (Set (Var "loc")))) & (Bool (Set (Var "loc"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))))))) ; 
 
theorem :: SCMFSA_3:13 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "da"))  ($#k14_scmfsa_2 :::":="::: )   "(" (Set (Var "f")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (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   ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))) & (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k2")))))))))))) ; 
 
theorem :: SCMFSA_3:14 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "," (Set (Var "db")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "f")) "," (Set (Var "db")) ")"   ($#k15_scmfsa_2 :::":="::: )  (Set (Var "da")))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (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   ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" ))) & (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "db")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "k1")) "," (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "k2")) "," (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" ) ")" )))))))))) ; 
 
theorem :: SCMFSA_3:15 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "da"))  ($#k16_scmfsa_2 :::":=len"::: )  (Set (Var "f")))) & (Bool (Set (Var "da"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k18_scmfsa_2 :::"."::: )  (Set (Var "f")) ")" )))))))))) ; 
 
theorem :: SCMFSA_3:16 (Bool  "for" (Set (Var "q")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_finset_1 :::"finite"::: )    ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  (Set (Var "b1"))  ($#v4_extpro_1 :::"-autonomic"::: )    ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s1"))) & (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Var "s2")))) "holds"  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P1"))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "da")) "being"   ($#m1_subset_1 :::"Int-Location":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_scmfsa_2 :::"FinSeq-Location"::: )    "st" (Bool (Bool (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k17_scmfsa_2 :::":=<0,...,0>"::: )  (Set (Var "da")))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p"))))) "holds"  (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   ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" ))) & (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "da")) ")" )))) "holds"  (Bool (Set (Set (Var "k1"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k2"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ))))))))))) ;