:: On state machines of calculating type :: by Hisayoshi Kunimune , Grzegorz Bancerek and Yatsuka Nakamura :: :: Received December 3, 2001 :: Copyright (c) 2001-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, XBOOLE_0, SUBSET_1, FINSEQ_1, FSM_1, ARYTM_3, FUNCT_1, XXREAL_0, ORDINAL4, FINSEQ_3, TARSKI, RELAT_1, PARTFUN1, CARD_1, NAT_1, CARD_5, ZFMISC_1, ARYTM_1, STRUCT_0, GLIB_000, FUNCOP_1, BINOP_1, ORDINAL1, ABSVALUE, MSUALG_1, FSM_2, FUNCT_7, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, NAT_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, STRUCT_0, FSM_1; constructors REAL_1, SQUARE_1, ABSVALUE, FUNCOP_1, FINSEQ_3, FINSEQ_4, BORSUK_1, FSM_1, VALUED_1, BINOP_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, NAT_1, FINSEQ_1, NAT_2, STRUCT_0, FSM_1, XREAL_0, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Calculating type reserve x,y for Real, i, j for non zero Element of NAT, I, O for non empty set, s,s1,s2,s3 for Element of I, w, w1, w2 for FinSequence of I, t for Element of O, S for non empty FSM over I, q, q1 for State of S; notation let I, S, q, w; synonym GEN(w,q) for (q,w)-admissible; end; registration let I, S, q, w; cluster GEN(w, q) -> non empty; end; theorem :: FSM_2:1 GEN(<*s*>, q) = <*q, (the Tran of S).[q, s]*>; theorem :: FSM_2:2 GEN(<*s1,s2*>, q) = <*q, (the Tran of S).[q, s1], (the Tran of S).[(the Tran of S).[q, s1], s2]*>; theorem :: FSM_2:3 GEN(<*s1,s2,s3*>, q) = <*q, (the Tran of S).[q, s1], (the Tran of S).[(the Tran of S).[q, s1], s2], (the Tran of S).[(the Tran of S).[(the Tran of S).[q, s1], s2],s3] *>; definition let I, S; attr S is calculating_type means :: FSM_2:def 1 for j holds for w1, w2 st w1.1 = w2.1 & j <= len(w1)+1 & j <= len(w2)+1 holds GEN(w1, the InitS of S).j = GEN(w2, the InitS of S).j; end; theorem :: FSM_2:4 S is calculating_type implies for w1, w2 st w1.1 = w2.1 holds GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable; theorem :: FSM_2:5 (for w1, w2 st w1.1 = w2.1 holds GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable) implies S is calculating_type; theorem :: FSM_2:6 S is calculating_type implies for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds GEN(w1, the InitS of S) = GEN(w2, the InitS of S); theorem :: FSM_2:7 (for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds GEN(w1, the InitS of S) = GEN(w2, the InitS of S)) implies S is calculating_type; definition let I, S, q, s; pred q is_accessible_via s means :: FSM_2:def 2 ex w be FinSequence of I st the InitS of S,<*s*>^w-leads_to q; end; definition let I, S, q; attr q is accessible means :: FSM_2:def 3 ex w be FinSequence of I st the InitS of S,w-leads_to q; end; theorem :: FSM_2:8 q is_accessible_via s implies q is accessible; theorem :: FSM_2:9 q is accessible & q <> the InitS of S implies ex s st q is_accessible_via s; theorem :: FSM_2:10 the InitS of S is accessible; theorem :: FSM_2:11 S is calculating_type & q is_accessible_via s implies ex m being non zero Element of NAT st for w st len w+1 >= m & w.1 = s holds q = GEN(w, the InitS of S).m & for i st i < m holds GEN(w, the InitS of S).i <> q; definition let I, S; attr S is regular means :: FSM_2:def 4 for q being State of S holds q is accessible; end; theorem :: FSM_2:12 (for s1,s2,q holds (the Tran of S).[q,s1] = (the Tran of S).[ q,s2]) implies S is calculating_type; theorem :: FSM_2:13 for S st (for s1,s2,q st q<>the InitS of S holds (the Tran of S).[q,s1] = (the Tran of S).[q,s2]) & for s,q1 holds (the Tran of S).[q1,s] <> the InitS of S holds S is calculating_type; theorem :: FSM_2:14 S is regular & S is calculating_type implies for s1, s2, q st q<>the InitS of S holds GEN(<*s1*>,q).2 = GEN(<*s2*>,q).2; theorem :: FSM_2:15 S is regular & S is calculating_type implies for s1, s2, q st q<>the InitS of S holds (the Tran of S).[q,s1] = (the Tran of S).[q,s2]; theorem :: FSM_2:16 S is regular & S is calculating_type implies for s, s1, s2, q st (the Tran of S).[the InitS of S,s1] <> (the Tran of S).[the InitS of S,s2] holds (the Tran of S).[q,s] <> the InitS of S; begin :: Machines with final states definition let I be set; struct (FSM over I) SM_Final over I (# carrier -> set, Tran -> Function of [: the carrier, I :], the carrier, InitS -> Element of the carrier, FinalS -> Subset of the carrier #); end; registration let I be set; cluster non empty for SM_Final over I; end; definition let I, s; let S be non empty SM_Final over I; pred s leads_to_final_state_of S means :: FSM_2:def 5 ex q being State of S st q is_accessible_via s & q in the FinalS of S; end; definition let I; let S be non empty SM_Final over I; attr S is halting means :: FSM_2:def 6 s leads_to_final_state_of S; end; definition let I be set, O be non empty set; struct (SM_Final over I, Moore-FSM over I, O) Moore-SM_Final over I,O (# carrier -> set, Tran -> Function of [: the carrier, I :], the carrier, OFun -> Function of the carrier, O, InitS -> Element of the carrier, FinalS -> Subset of the carrier #); end; registration let I be set, O be non empty set; cluster non empty strict for Moore-SM_Final over I, O; end; definition let I, O; let i,f be set; let o be Function of {i,f}, O; func I-TwoStatesMooreSM(i,f,o) -> non empty strict Moore-SM_Final over I, O means :: FSM_2:def 7 the carrier of it = {i,f} & the Tran of it = [:{i,f}, I :] --> f & the OFun of it = o & the InitS of it = i & the FinalS of it = {f}; end; theorem :: FSM_2:17 for i,f being set, o being Function of {i,f}, O for j st 1 < j & j <= len w+1 holds GEN(w, the InitS of I-TwoStatesMooreSM(i,f,o)).j = f; registration let I, O; let i,f be set; let o be Function of {i,f}, O; cluster I-TwoStatesMooreSM(i,f,o) -> calculating_type; end; registration let I, O; let i,f be set; let o be Function of {i,f}, O; cluster I-TwoStatesMooreSM(i,f,o) -> halting; end; reserve n, m, o, p for non zero Element of NAT, M for non empty Moore-SM_Final over I, O, q for State of M; theorem :: FSM_2:18 M is calculating_type & s leads_to_final_state_of M implies ex m being non zero Element of NAT st (for w st len w+1 >= m & w.1 = s holds GEN(w, the InitS of M).m in the FinalS of M) & for w,j st j <= len w +1 & w.1 = s & j < m holds not GEN(w, the InitS of M).j in the FinalS of M; begin :: Correctness of a result of state machine definition let I, O, M, s; let t be object; pred t is_result_of s,M means :: FSM_2:def 8 ex m st for w st w.1=s holds (m <= len w+1 implies t = (the OFun of M).(GEN(w, the InitS of M).m) & GEN(w, the InitS of M).m in the FinalS of M) & for n st n < m & n <= len w+1 holds not GEN(w, the InitS of M).n in the FinalS of M; end; theorem :: FSM_2:19 the InitS of M in the FinalS of M implies (the OFun of M).the InitS of M is_result_of s, M; theorem :: FSM_2:20 M is calculating_type & s leads_to_final_state_of M implies ex t st t is_result_of s, M; theorem :: FSM_2:21 s leads_to_final_state_of M implies for t1, t2 being Element of O st t1 is_result_of s, M & t2 is_result_of s, M holds t1 = t2; theorem :: FSM_2:22 for X being non empty set for f being BinOp of X for M being non empty Moore-SM_Final over [:X, X:], succ X st M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & for x,y being Element of X holds (the Tran of M).[the InitS of M, [x,y]] = f.(x,y) holds M is halting & for x,y being Element of X holds f.(x,y) is_result_of [x,y], M; theorem :: FSM_2:23 for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x) & (for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y) for x,y being Element of REAL holds max(x,y) is_result_of [x,y], M; theorem :: FSM_2:24 for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x) & (for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y) for x,y being Element of REAL holds min(x,y) is_result_of [x,y], M; theorem :: FSM_2:25 for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x+y) for x,y being Element of REAL holds x+y is_result_of [x,y], M; theorem :: FSM_2:26 for M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1) & (for x,y st (x=0 or y=0) & x <= 0 & y <=0 holds (the Tran of M).[the InitS of M, [x,y]] = 0) & (for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1) for x,y being Element of REAL holds max(sgn x,sgn y) is_result_of [x,y], M; registration let I, O; cluster calculating_type halting for non empty Moore-SM_Final over I, O; end; registration let I; cluster calculating_type halting for non empty SM_Final over I; end; definition let I, O; let M be calculating_type halting non empty Moore-SM_Final over I, O; let s; func Result(s, M) -> Element of O means :: FSM_2:def 9 it is_result_of s, M; end; theorem :: FSM_2:27 for f being Function of {0, 1}, O holds Result(s, I-TwoStatesMooreSM(0,1,f)) = f.1; theorem :: FSM_2:28 for M being calculating_type halting non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x) & (for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y) for x,y being Element of REAL holds Result([x,y], M) = max(x,y); theorem :: FSM_2:29 for M being calculating_type halting non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x) & (for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y) for x,y being Element of REAL holds Result([x,y], M) = min(x,y); theorem :: FSM_2:30 for M being calculating_type halting non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x+y) for x,y being Element of REAL holds Result([x,y], M) = x+y; theorem :: FSM_2:31 for M being calculating_type halting non empty Moore-SM_Final over [:REAL, REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & (for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1) & (for x,y st (x=0 or y=0) & x <= 0 & y <=0 holds (the Tran of M).[the InitS of M, [x,y]] = 0) & (for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1) for x,y being Element of REAL holds Result([x,y], M) = max(sgn x, sgn y);