:: SCMFSA_5  semantic presentation begin  




begin  
theorem :: SCMFSA_5:1 (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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 "b2"))  ($#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   ($#k9_memstr_0 :::"IncIC"::: )   "(" (Set (Var "p")) "," (Set (Var "k")) ")" )  ($#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   ($#k6_compos_1 :::"Reloc"::: )   "(" (Set (Var "q")) "," (Set (Var "k")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "P2")))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" ))) & (Bool (Set   ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set  "("  ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P1")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" ) ")"  ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_extpro_1 :::"CurInstr"::: )   "(" (Set (Var "P2")) "," (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" ) ")" )) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "p")) ")" ) ")" ))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P1")) "," (Set  "(" (Set (Var "s1"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2")) ")" ) ")" ) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")"  ")" )))  ")" ))))))) ; 
 registration
cluster (Set   ($#k1_scmfsa_2 :::"SCM+FSA"::: )  ) ->   ($#v5_amistd_5 :::"relocable1"::: )     ($#v6_amistd_5 :::"relocable2"::: )   ; 
end;