:: SF_MASTR semantic presentation begin theorem :: SF_MASTR:1 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Set (Var "a1")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b2"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ; theorem :: SF_MASTR:2 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ; theorem :: SF_MASTR:3 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ; theorem :: SF_MASTR:4 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ; theorem :: SF_MASTR:5 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a1")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a2")) "," (Set (Var "b2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ; theorem :: SF_MASTR:6 (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l2"))))) "holds" (Bool (Set (Var "l1")) ($#r1_hidden :::"="::: ) (Set (Var "l2")))) ; theorem :: SF_MASTR:7 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "a1")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l2"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "l1")) ($#r1_hidden :::"="::: ) (Set (Var "l2"))) ")" ))) ; theorem :: SF_MASTR:8 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "a1")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l2"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "l1")) ($#r1_hidden :::"="::: ) (Set (Var "l2"))) ")" ))) ; theorem :: SF_MASTR:9 (Bool "for" (Set (Var "b1")) "," (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Set (Var "b1")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f1")) "," (Set (Var "a1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f2")) "," (Set (Var "a2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))) ")" ))) ; theorem :: SF_MASTR:10 (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set "(" (Set (Var "f1")) "," (Set (Var "a1")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f2")) "," (Set (Var "a2")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b2"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))) ")" ))) ; theorem :: SF_MASTR:11 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Set (Var "a1")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f2"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))) ")" ))) ; theorem :: SF_MASTR:12 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a2"))))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))) ")" ))) ; begin definitionlet "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"UsedIntLoc"::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) )) means :: SF_MASTR:def 1 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool "(" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")))) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) )) ")" )) if (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k3_enumset1 :::"}"::: ) )) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")))) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) )) ")" ))) if (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 7)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 8)) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) )) ")" ))) if (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 10)) ")" ) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) )) ")" ))) if (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 12)) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"UsedIntLoc"::: SF_MASTR:def 1 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k3_enumset1 :::"}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) )) ")" )) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 7)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 8)) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) )) ")" ))) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 10)) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) )) ")" ))) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 12)) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) )) ")" ))) ")" ) ")" & (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k3_enumset1 :::"}"::: ) )) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 7)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 8)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 10)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 12)) "or" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ) ")" ))); theorem :: SF_MASTR:13 (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: SF_MASTR:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) "holds" (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) )))) ; theorem :: SF_MASTR:15 (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: SF_MASTR:16 (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"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")))) ")" )) "holds" (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ))))) ; theorem :: SF_MASTR:17 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k5_scmfsa_m :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k5_scmfsa_m :::"}"::: ) ))))) ; theorem :: SF_MASTR:18 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set (Var "a")) ($#k4_scmfsa_m :::"}"::: ) ))))) ; definitionlet "p" be ($#m1_hidden :::"Function":::); func :::"UsedIntLoc"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) means :: SF_MASTR:def 2 (Bool "ex" (Set (Var "UIL")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set (Var "UIL")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set (Var "UIL")) ($#k3_relat_1 :::"*"::: ) "p" ")" ))) ")" )); end; :: deftheorem defines :::"UsedIntLoc"::: SF_MASTR:def 2 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "UIL")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set (Var "UIL")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set (Var "UIL")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")) ")" ))) ")" )) ")" ))); registrationlet "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: SF_MASTR:19 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))))) ; theorem :: SF_MASTR:20 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "r")) ")" )))) ; theorem :: SF_MASTR:21 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "r"))))) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "r")) ")" )))) ; theorem :: SF_MASTR:22 (Bool "for" (Set (Var "p")) "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 ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:23 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "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 ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:24 (Bool "for" (Set (Var "p")) "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 ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:25 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:26 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" )))) ; theorem :: SF_MASTR:27 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" )))) ; theorem :: SF_MASTR:28 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i"))))) ; theorem :: SF_MASTR:29 (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 ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "J")) ")" ))))) ; theorem :: SF_MASTR:30 (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 ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "j")) ")" ))))) ; theorem :: SF_MASTR:31 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set "(" (Set (Var "i")) ($#k6_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "j")) ")" )))) ; begin definitionlet "i" be ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"UsedInt*Loc"::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) )) means :: SF_MASTR:def 3 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ")" ))) if (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 10)) ")" ) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))) "or" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ")" ))) if (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) "i") ($#r1_hidden :::"="::: ) (Num 12)) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"UsedInt*Loc"::: SF_MASTR:def 3 : (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) )) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 10)) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ")" ))) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 12)) ")" )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ")" ))) ")" ) ")" & (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 10)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 12)) "or" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ) ")" ))); theorem :: SF_MASTR:32 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "l")) "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 "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_2 :::"goto"::: ) (Set (Var "l")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l")))) ")" )) "holds" (Bool (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: SF_MASTR:33 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: SF_MASTR:34 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))))) ; definitionlet "p" be ($#m1_hidden :::"Function":::); func :::"UsedInt*Loc"::: "p" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) means :: SF_MASTR:def 4 (Bool "ex" (Set (Var "UIL")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set (Var "UIL")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set (Var "UIL")) ($#k3_relat_1 :::"*"::: ) "p" ")" ))) ")" )); end; :: deftheorem defines :::"UsedInt*Loc"::: SF_MASTR:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "UIL")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set (Set (Var "UIL")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")))) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set (Var "UIL")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")) ")" ))) ")" )) ")" ))); registrationlet "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: SF_MASTR:35 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")))))) ; theorem :: SF_MASTR:36 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "r")) ")" )))) ; theorem :: SF_MASTR:37 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "r"))))) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "r")) ")" )))) ; theorem :: SF_MASTR:38 (Bool "for" (Set (Var "p")) "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 ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:39 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "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 ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k5_compos_0 :::"IncAddr"::: ) "(" (Set (Var "i")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:40 (Bool "for" (Set (Var "p")) "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 ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k5_compos_1 :::"IncAddr"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:41 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k6_compos_1 :::"Reloc"::: ) "(" (Set (Var "I")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: SF_MASTR:42 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k2_scmfsa6a :::"Directed"::: ) (Set (Var "I")) ")" )))) ; theorem :: SF_MASTR:43 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Program":::) "of" "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "I")) ($#k3_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "J")) ")" )))) ; theorem :: SF_MASTR:44 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" ($#k11_compos_1 :::"Macro"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i"))))) ; theorem :: SF_MASTR:45 (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 ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "i")) ($#k4_scmfsa6a :::"";""::: ) (Set (Var "J")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "J")) ")" ))))) ; theorem :: SF_MASTR:46 (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 ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "I")) ($#k5_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "j")) ")" ))))) ; theorem :: SF_MASTR:47 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set "(" (Set (Var "i")) ($#k6_scmfsa6a :::"";""::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "j")) ")" )))) ; begin definitioncanceled; end; :: deftheorem SF_MASTR:def 5 : canceled; theorem :: SF_MASTR:48 (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 :: SF_MASTR:49 (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 "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"FirstNotUsed"::: "p" -> ($#m1_subset_1 :::"Int-Location":::) means :: SF_MASTR:def 6 (Bool "ex" (Set (Var "sil")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) "st" (Bool "(" (Bool (Set (Var "sil")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) "p" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmfsa_m :::"}"::: ) ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa_m :::"FirstNotIn"::: ) (Set (Var "sil")))) ")" )); end; :: deftheorem defines :::"FirstNotUsed"::: SF_MASTR:def 6 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "sil")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_scmfsa_2 :::"Int-Locations"::: ) ) "st" (Bool "(" (Bool (Set (Var "sil")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_scmfsa_m :::"{"::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_scmfsa_m :::"}"::: ) ))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa_m :::"FirstNotIn"::: ) (Set (Var "sil")))) ")" )) ")" ))); registrationlet "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); cluster (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) "p") -> ($#v1_scmfsa_m :::"read-write"::: ) ; end; theorem :: SF_MASTR:50 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Bool "not" (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "p")))))) ; theorem :: SF_MASTR:51 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set ($#k9_scmfsa_2 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set ($#k10_scmfsa_2 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" ))) ; theorem :: SF_MASTR:52 (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"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "a")) ($#k12_scmfsa_2 :::"=0_goto"::: ) (Set (Var "l"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set (Set (Var "a")) ($#k13_scmfsa_2 :::">0_goto"::: ) (Set (Var "l"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" )) "holds" (Bool (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))))) ; theorem :: SF_MASTR:53 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" )))) ; theorem :: SF_MASTR:54 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" )) "holds" (Bool (Set ($#k5_sf_mastr :::"FirstNotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))))) ; begin definitioncanceled; end; :: deftheorem SF_MASTR:def 7 : canceled; theorem :: SF_MASTR:55 (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 :: SF_MASTR:56 (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"))))) ; definitionlet "p" be ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ); func :::"First*NotUsed"::: "p" -> ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) means :: SF_MASTR:def 8 (Bool "ex" (Set (Var "sil")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) "st" (Bool "(" (Bool (Set (Var "sil")) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) "p")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_scmfsa_m :::"First*NotIn"::: ) (Set (Var "sil")))) ")" )); end; :: deftheorem defines :::"First*NotUsed"::: SF_MASTR:def 8 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_sf_mastr :::"First*NotUsed"::: ) (Set (Var "p")))) "iff" (Bool "ex" (Set (Var "sil")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_scmfsa_2 :::"FinSeq-Locations"::: ) ) "st" (Bool "(" (Bool (Set (Var "sil")) ($#r1_hidden :::"="::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_scmfsa_m :::"First*NotIn"::: ) (Set (Var "sil")))) ")" )) ")" ))); theorem :: SF_MASTR:57 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "holds" (Bool (Bool "not" (Set ($#k6_sf_mastr :::"First*NotUsed"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "p")))))) ; theorem :: SF_MASTR:58 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "b")) ($#k14_scmfsa_2 :::":="::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "a")) ")" ($#k15_scmfsa_2 :::":="::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" )) "holds" (Bool (Set ($#k6_sf_mastr :::"First*NotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "f")))))) ; theorem :: SF_MASTR:59 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"preProgram":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "a")) ($#k16_scmfsa_2 :::":=len"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) "or" (Bool (Set (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p")))) ")" )) "holds" (Bool (Set ($#k6_sf_mastr :::"First*NotUsed"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "f")))))) ; begin theorem :: SF_MASTR:60 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Int-Location":::) (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"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")))))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))))))) ; theorem :: SF_MASTR:61 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "I")))) ")" ) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))))) ; theorem :: SF_MASTR:62 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (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"::: ) ) "st" (Bool (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")))))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))) ; theorem :: SF_MASTR:63 (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "I")))) ")" ) & (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "n")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))))))))) ; theorem :: SF_MASTR:64 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")) ")" ))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "t"))))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "t")) ")" ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "t")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k1_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "s")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "i")) "," (Set (Var "t")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k3_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "i")) ")" ))) ")" ))) ; theorem :: SF_MASTR:65 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Program":::) "of" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "s"))) & (Bool (Set ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I")) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "I")))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "t")) "," (Set (Var "m")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "I")))) ")" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "t")) "," (Set (Var "m")) ")" ")" ))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sf_mastr :::"UsedIntLoc"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "t")) "," (Set (Var "m")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_sf_mastr :::"UsedInt*Loc"::: ) (Set (Var "I"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "m")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "Q")) "," (Set (Var "t")) "," (Set (Var "m")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" ) ")" ))))) ;