Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

The abstract of the Mizar article:

On State Machines of Calculating Type

by
Hisayoshi Kunimune,
Grzegorz Bancerek, and
Yatsuka Nakamura

Received December 3, 2001

MML identifier: FSM_2
[ Mizar article, MML identifier index ]


environ

 vocabulary FINSEQ_1, ARYTM_1, FUNCT_1, RELAT_1, BOOLE, AMI_1, MATRIX_2,
      CARD_5, FSM_1, FSM_2, ZFMISC_1, PARTFUN1, BINOP_1, FUNCOP_1, SQUARE_1,
      ABSVALUE, REALSET1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, MATRIX_2,
      FINSEQ_1, FINSEQ_4, STRUCT_0, BORSUK_1, FSM_1, SCMPDS_1, SQUARE_1,
      ABSVALUE, REALSET1;
 constructors REAL_1, DOMAIN_1, BORSUK_1, MATRIX_2, FSM_1, REALSET1, FINSEQ_4,
      SCMPDS_1, LIMFUNC1, BINARITH, MEMBERED;
 clusters SUBSET_1, RELSET_1, FINSEQ_1, FSM_1, NAT_2, STRUCT_0, XBOOLE_0,
      REALSET1, NAT_1, XREAL_0, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Calculating type

reserve
        x,y for Real,
        i, j, h for non empty 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;

definition let I, S, q, w;
 redefine func (q,w)-admissible;
 synonym GEN(w,q);
end;

definition 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 empty 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;

definition let I be set;
  cluster non empty 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;

definition let I be set, O be non empty set;
  cluster non empty strict 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;

definition
 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;

definition
 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 empty 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 &
 not the InitS of M in the FinalS of M
 implies
  ex m being non empty 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 set;
  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 &
 not the InitS of M in the FinalS of M
 implies
  ex t st t is_result_of s, M;

theorem :: FSM_2:21
 M is calculating_type & 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:], X \/ {X}
  st M is calculating_type &
     the carrier of M = X \/ {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:], REAL \/ {REAL}
  st M is calculating_type &
     the carrier of M = REAL \/ {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:], REAL \/ {REAL}
  st M is calculating_type &
     the carrier of M = REAL \/ {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:], REAL \/ {REAL}
  st M is calculating_type &
     the carrier of M = REAL \/ {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:], REAL \/ {REAL}
  st M is calculating_type &
     the carrier of M = REAL \/ {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;

definition
 let I, O;
 cluster calculating_type halting (non empty Moore-SM_Final over I, O);
end;

definition
 let I;
 cluster calculating_type halting (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:], REAL \/ {REAL})
  st the carrier of M = REAL \/ {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:], REAL \/ {REAL})
  st the carrier of M = REAL \/ {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:], REAL \/ {REAL})
  st the carrier of M = REAL \/ {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:], REAL \/ {REAL})
  st the carrier of M = REAL \/ {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);

Back to top