:: SCMFSA6A  semantic presentation begin  














definitionlet "P" be (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"::: )    ($#m1_hidden :::"Function":::); let "l" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"Directed":::  "(" "P" "," "l" ")"  ->   ($#m1_hidden :::"preProgram":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA6A:def 1 (Set "P"  ($#k6_funct_4 :::"+~"::: )   "(" (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  "l" ")" ) ")" ); end; 






:: deftheorem    defines :::"Directed"::: SCMFSA6A:def 1 :  (Bool  "for" (Set (Var "P")) "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"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_scmfsa6a :::"Directed"::: )   "(" (Set (Var "P")) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k6_funct_4 :::"+~"::: )   "(" (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) "," (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set (Var "l")) ")" ) ")" )))); 
 definitionlet "P" be (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"::: )    ($#m1_hidden :::"Function":::); func  :::"Directed"::: "P" ->   ($#m1_hidden :::"preProgram":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) equals :: SCMFSA6A:def 2 (Set   ($#k1_scmfsa6a :::"Directed"::: )   "(" "P" "," (Set  "("  ($#k5_card_1 :::"card"::: )  "P" ")" ) ")" ); end; 





:: deftheorem    defines :::"Directed"::: SCMFSA6A:def 2 :  (Bool  "for" (Set (Var "P")) "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"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k2_scmfsa6a :::"Directed"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_scmfsa6a :::"Directed"::: )   "(" (Set (Var "P")) "," (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "P")) ")" ) ")" ))); 
 registrationlet "I" be   ($#m1_hidden :::"Program":::) "of" ; 
cluster (Set   ($#k2_scmfsa6a :::"Directed"::: )  "I") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_afinsq_1 :::"initial"::: )   ; 
end; 
theorem :: SCMFSA6A:1 (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   "holds" (Bool (Bool  "not" (Set   ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_scmfsa6a :::"Directed"::: )  (Set (Var "I")) ")" ))))) ; 
 
theorem :: SCMFSA6A:2 (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k6_compos_1 :::"Reloc"::: )   "(" (Set  "("  ($#k2_scmfsa6a :::"Directed"::: )  (Set (Var "I")) ")" ) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_compos_1 :::"InstructionsF"::: )  "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )  ($#k16_funcop_1 :::".-->"::: )  (Set  "("  ($#k11_scmfsa_2 :::"goto"::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k6_compos_1 :::"Reloc"::: )   "(" (Set (Var "I")) "," (Set (Var "m")) ")"  ")" ))))) ; 
 












theorem :: SCMFSA6A:3 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "holds"  (Bool  "("  (Bool (Set   ($#k2_compos_0 :::"InsCode"::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set  ($#k9_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 6) "," (Num 7) "," (Num 8) ($#k9_domain_1 :::"}"::: ) )) "or" (Bool (Set (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k4_struct_0 :::"IC"::: )   ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s")) ")" )))  ")" ))) ; 
 
theorem :: SCMFSA6A:4 canceled; 
 
theorem :: SCMFSA6A:5 canceled; 
 
theorem :: SCMFSA6A:6 canceled; 
 
theorem :: SCMFSA6A:7 canceled; 
 
theorem :: SCMFSA6A:8 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  "st" (Bool (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set (Var "s2")))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set (Var "s2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s1")) ")"  ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "("  ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "s2")) ")"  ")" ))) & (Bool (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set (Var "i")) "," (Set (Var "s1")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_memstr_0 :::"DataPart"::: )  (Set  "("  ($#k2_extpro_1 :::"Exec"::: )   "(" (Set  "("  ($#k5_compos_0 :::"IncAddr"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "s2")) ")"  ")" )))  ")" )))) ; 
 
theorem :: SCMFSA6A:9 canceled; 
 
theorem :: SCMFSA6A:10 canceled; 
 
theorem :: SCMFSA6A:11 canceled; 
 
theorem :: SCMFSA6A:12 canceled; 
 
theorem :: SCMFSA6A:13 canceled; 
 
theorem :: SCMFSA6A:14 canceled; 
 begin  definitioncanceled; let "I", "J" be   ($#m1_hidden :::"Program":::) "of" ; func "I" :::"";""::: "J" ->   ($#m1_hidden :::"Program":::) "of"  equals :: SCMFSA6A:def 4 (Set (Set  "("  ($#k2_scmfsa6a :::"Directed"::: )  (Set  "("  ($#k63_valued_1 :::"CutLastLoc"::: )  (Set  "("  ($#k10_compos_1 :::"stop"::: )  "I" ")" ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k6_compos_1 :::"Reloc"::: )   "(" "J" "," (Set  "("  ($#k5_card_1 :::"card"::: )  "I" ")" ) ")"  ")" )); end; 






:: deftheorem   SCMFSA6A:def 3 :  canceled;  
 
:: deftheorem    defines :::"";""::: SCMFSA6A:def 4 :  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_scmfsa6a :::"Directed"::: )  (Set  "("  ($#k63_valued_1 :::"CutLastLoc"::: )  (Set  "("  ($#k10_compos_1 :::"stop"::: )  (Set (Var "I")) ")" ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k6_compos_1 :::"Reloc"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" ) ")"  ")" )))); 
 registrationlet "I" be   ($#m1_hidden :::"Program":::) "of" ; let "J" be  ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )   ($#m1_hidden :::"Program":::) "of" ; 
cluster (Set "I"  ($#k3_scmfsa6a :::"";""::: )  "J") ->  ($#~v2_compos_1  "non"   ($#v2_compos_1 :::"halt-free"::: )   )  ; 
end; 
theorem :: SCMFSA6A:15 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "I")))) & (Bool (Set (Set (Var "I"))  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )))) "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))))) ; 
 
theorem :: SCMFSA6A:16 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k2_scmfsa6a :::"Directed"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J"))))) ; 
 
theorem :: SCMFSA6A:17 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "I")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" )))) ; 
 
theorem :: SCMFSA6A:18 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set (Var "I"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J"))))) ; 
 begin  definitionlet "i" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "J" be   ($#m1_hidden :::"Program":::) "of" ; func "i" :::"";""::: "J" ->   ($#m1_hidden :::"Program":::) "of"  equals :: SCMFSA6A:def 5 (Set (Set  "("  ($#k11_compos_1 :::"Macro"::: )  "i" ")" )  ($#k3_scmfsa6a :::"";""::: )  "J"); end; 






:: deftheorem    defines :::"";""::: SCMFSA6A:def 5 :  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set (Var "J")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "i")) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")))))); 
 definitionlet "I" be   ($#m1_hidden :::"Program":::) "of" ; let "j" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func "I" :::"";""::: "j" ->   ($#m1_hidden :::"Program":::) "of"  equals :: SCMFSA6A:def 6 (Set "I"  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  "j" ")" )); end; 






:: deftheorem    defines :::"";""::: SCMFSA6A:def 6 :  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"   (Bool  "for" (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "j")) ")" ))))); 
 definitionlet "i", "j" be   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func "i" :::"";""::: "j" ->   ($#m1_hidden :::"Program":::) "of"  equals :: SCMFSA6A:def 7 (Set (Set  "("  ($#k11_compos_1 :::"Macro"::: )  "i" ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  "j" ")" )); end; 






:: deftheorem    defines :::"";""::: SCMFSA6A:def 7 :  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "i")) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "j")) ")" )))); 
 
theorem :: SCMFSA6A:19 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "i")) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j"))))) ; 
 
theorem :: SCMFSA6A:20 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set  "("  ($#k11_compos_1 :::"Macro"::: )  (Set (Var "j")) ")" )))) ; 
 
theorem :: SCMFSA6A:21 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "J")) ")" )))) ; 
 registrationlet "P" be   ($#m1_hidden :::"preProgram":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); let "l" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k1_scmfsa6a :::"Directed"::: )   "(" "P" "," "l" ")" ) ->   ($#v2_compos_1 :::"halt-free"::: )   ; 
end; registrationlet "P" be   ($#m1_hidden :::"preProgram":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); 
cluster (Set   ($#k2_scmfsa6a :::"Directed"::: )  "P") ->   ($#v2_compos_1 :::"halt-free"::: )   ; 
end; 
theorem :: SCMFSA6A:22 (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"preProgram":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "I")) "is"   ($#v2_compos_1 :::"halt-free"::: )  )) "holds"  (Bool (Set   ($#k1_scmfsa6a :::"Directed"::: )   "(" (Set (Var "I")) "," (Set (Var "l")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "I"))))) ; 
 
theorem :: SCMFSA6A:23 (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"preProgram":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k6_compos_1 :::"Reloc"::: )   "(" (Set  "("  ($#k2_scmfsa6a :::"Directed"::: )  (Set (Var "I")) ")" ) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_scmfsa6a :::"Directed"::: )   "(" (Set  "("  ($#k6_compos_1 :::"Reloc"::: )   "(" (Set (Var "I")) "," (Set (Var "k")) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ) ")" )))) ; 
 
theorem :: SCMFSA6A:24 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k2_scmfsa6a :::"Directed"::: )  (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set  "("  ($#k2_scmfsa6a :::"Directed"::: )  (Set (Var "J")) ")" )))) ; 
 
theorem :: SCMFSA6A:25 (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "J"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "K")) ")" )))) ; 
 
theorem :: SCMFSA6A:26 (Bool  "for" (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "," (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "J"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMFSA6A:27 (Bool  "for" (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "j"))  ($#k4_scmfsa6a :::"";""::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SCMFSA6A:28 (Bool  "for" (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k3_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "j"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMFSA6A:29 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "J")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "J"))  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SCMFSA6A:30 (Bool  "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "J"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: SCMFSA6A:31 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" )  ($#k3_scmfsa6a :::"";""::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "j"))  ($#k4_scmfsa6a :::"";""::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SCMFSA6A:32 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" )  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set  "(" (Set (Var "j"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "k")) ")" )))) ; 
 
theorem :: SCMFSA6A:33 (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "i"))  ($#k4_scmfsa6a :::"";""::: )  (Set (Var "J")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "J")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2))))) ; 
 
theorem :: SCMFSA6A:34 (Bool  "for" (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Program":::) "of"  "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "I"))  ($#k5_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2))))) ; 
 
theorem :: SCMFSA6A:35 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_subset_1 :::"Instruction":::) "of" (Set  ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "i"))  ($#k6_scmfsa6a :::"";""::: )  (Set (Var "j")) ")" ))  ($#r1_hidden :::"="::: )  (Num 4))) ;