:: SCMFSA_7 semantic presentation begin definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "k" be ($#m1_hidden :::"Integer":::); func "a" :::":="::: "k" -> (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":::) means :: SCMFSA_7:def 1 (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) "k") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "a" ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "a" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )) if (Bool "k" ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_xcmplx_0 :::"+"::: ) "k") ($#r1_hidden :::"="::: ) (Num 1)) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "a" ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "a" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )); end; :: deftheorem defines :::":="::: SCMFSA_7:def 1 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b3")) "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 "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_scmfsa_7 :::":="::: ) (Set (Var "k")))) "iff" (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_scmfsa_7 :::":="::: ) (Set (Var "k")))) "iff" (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )) ")" ) ")" ")" )))); definitionlet "a" be ($#m1_subset_1 :::"Int-Location":::); let "k" be ($#m1_hidden :::"Integer":::); func :::"aSeq"::: "(" "a" "," "k" ")" -> ($#m1_hidden :::"XFinSequence":::) "of" means :: SCMFSA_7:def 2 (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) "k") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "a" ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" "a" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ))) ")" )) if (Bool "k" ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_xcmplx_0 :::"+"::: ) "k") ($#r1_hidden :::"="::: ) (Num 1)) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "a" ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" "a" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"aSeq"::: SCMFSA_7:def 2 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" )) "iff" (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k7_scmfsa_2 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" )) "iff" (Bool "ex" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "k1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "k1")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ))) ")" )) ")" ) ")" ")" )))); theorem :: SCMFSA_7:1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_scmfsa_7 :::":="::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))))) ; definitionlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); func :::"aSeq"::: "(" "f" "," "p" ")" -> ($#m1_hidden :::"XFinSequence":::) "of" means :: SCMFSA_7:def 3 (Bool "ex" (Set (Var "pp")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "pp"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "pp"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "pp")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "(" "f" "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "pp")))) ")" )); end; :: deftheorem defines :::"aSeq"::: SCMFSA_7:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" )) "iff" (Bool "ex" (Set (Var "pp")) "being" ($#m1_hidden :::"XFinSequence":::) "of" "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "pp"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "pp"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "pp")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "(" (Set (Var "f")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ($#k15_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))) ")" )) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "pp")))) ")" )) ")" )))); definitionlet "f" be ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); func "f" :::":="::: "p" -> (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":::) equals :: SCMFSA_7:def 4 (Set (Set "(" (Set "(" (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" "f" ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k3_scmfsa_7 :::"aSeq"::: ) "(" "f" "," "p" ")" ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )); end; :: deftheorem defines :::":="::: SCMFSA_7:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k4_scmfsa_7 :::":="::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "f")) ($#k17_scmfsa_2 :::":=<0,...,0>"::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k3_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "f")) "," (Set (Var "p")) ")" ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))))); theorem :: SCMFSA_7:2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_scmfsa_7 :::":="::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )))) ; theorem :: SCMFSA_7:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_scmfsa_7 :::":="::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set (Var "a")) ($#k6_scmfsa_2 :::":="::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k8_scmfsa_2 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )))) ; theorem :: SCMFSA_7:4 (Bool "for" (Set (Var "P")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c0")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set (Var "b2")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afinsq_1 :::"dom"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_compos_1 :::"."::: ) (Set "(" (Set (Var "c0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c0")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" ) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" )))))) ; theorem :: SCMFSA_7:5 (Bool "for" (Set (Var "P")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" )))) "holds" (Bool "(" (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ) ")" ) & (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k2_scmfsa_7 :::"aSeq"::: ) "(" (Set (Var "a")) "," (Set (Var "k")) ")" ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ))))) ; theorem :: SCMFSA_7:6 (Bool "for" (Set (Var "P")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Int-Location":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k1_scmfsa_7 :::":="::: ) (Set (Var "k"))) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f")))) ")" ) ")" ))))) ; theorem :: SCMFSA_7:7 (Bool "for" (Set (Var "P")) "being" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_scmfsa_2 :::"SCM+FSA"::: ) ) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_scmfsa_2 :::"intloc"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k4_scmfsa_7 :::":="::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "P")))) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Int-Location":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Num 1))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_scmfsa_2 :::"intloc"::: ) (Num 2)))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_scmfsa_2 :::"FinSeq-Location"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set (Var "f")))) "holds" (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "P")) "," (Set (Var "s")) ")" ")" ) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k18_scmfsa_2 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))))) ;