fsm_1.miz



    begin

    reserve m,n,i,k for Nat;

    definition

      let IAlph be set;

      struct ( 1-sorted) FSM over IAlph (# the carrier -> set,

the Tran -> Function of [: the carrier, IAlph:], the carrier,

the InitS -> Element of the carrier #)

       attr strict strict;

    end

    definition

      let IAlph be set, fsm be FSM over IAlph;

      mode State of fsm is Element of fsm;

    end

    registration

      let X be set;

      cluster non empty finite for FSM over X;

      existence

      proof

        set A = the non empty finite set, T = the Function of [:A, X:], A, I = the Element of A;

        take S = FSM (# A, T, I #);

        thus S is non empty;

        thus thesis;

      end;

    end

    reserve IAlph,OAlph for non empty set,

fsm for non empty FSM over IAlph,

s for Element of IAlph,

w,w1,w2 for FinSequence of IAlph,

q,q9,q1,q2 for State of fsm;

    definition

      let IAlph be non empty set;

      let fsm be non empty FSM over IAlph;

      let s be Element of IAlph, q be State of fsm;

      :: FSM_1:def1

      func s -succ_of q -> State of fsm equals (the Tran of fsm . [q, s]);

      correctness ;

    end

    definition

      let IAlph be non empty set;

      let fsm be non empty FSM over IAlph;

      let q be State of fsm;

      let w be FinSequence of IAlph;

      :: FSM_1:def2

      func (q,w) -admissible -> FinSequence of the carrier of fsm means

      : Def2: (it . 1) = q & ( len it ) = (( len w) + 1) & for i be Nat st 1 <= i & i <= ( len w) holds ex wi be Element of IAlph, qi,qi1 be State of fsm st wi = (w . i) & qi = (it . i) & qi1 = (it . (i + 1)) & (wi -succ_of qi) = qi1;

      existence

      proof

        set N = (( len w) + 1);

        set D = the carrier of fsm;

        defpred P[ Nat, set, set] means ex wn be Element of IAlph, q9,q99 be Element of D st (w . $1) = wn & q9 = $2 & q99 = $3 & (wn -succ_of q9) = q99;

        

         A1: for n be Nat st 1 <= n & n < N holds for x be Element of D holds ex y be Element of D st P[n, x, y]

        proof

          let n be Nat;

          assume

           A2: 1 <= n;

          assume n < N;

          then n <= ( len w) by NAT_1: 13;

          then n in ( dom w) by A2, FINSEQ_3: 25;

          then

          reconsider wn = (w . n) as Element of IAlph by FINSEQ_2: 11;

          let x be Element of D;

          (wn -succ_of x) = (the Tran of fsm . [x, wn]);

          hence thesis;

        end;

        consider p be FinSequence of D such that

         A3: ( len p) = N & ((p . 1) = q or N = 0 ) & for n be Nat st 1 <= n & n < N holds P[n, (p . n), (p . (n + 1))] from RECDEF_1:sch 4( A1);

        take p;

        thus (p . 1) = q by A3;

        thus ( len p) = (( len w) + 1) by A3;

        let i be Nat;

        assume

         A4: 1 <= i;

        assume i <= ( len w);

        then i in NAT & i < N by NAT_1: 13, ORDINAL1:def 12;

        hence thesis by A3, A4;

      end;

      uniqueness

      proof

        let qs1,qs2 be FinSequence of the carrier of fsm such that

         A5: (qs1 . 1) = q and

         A6: ( len qs1) = (( len w) + 1) and

         A7: for i be Nat st 1 <= i & i <= ( len w) holds ex wi be Element of IAlph, qs1i,qs1i1 be State of fsm st wi = (w . i) & qs1i = (qs1 . i) & qs1i1 = (qs1 . (i + 1)) & (wi -succ_of qs1i) = qs1i1 and

         A8: (qs2 . 1) = q and

         A9: ( len qs2) = (( len w) + 1) and

         A10: for i be Nat st 1 <= i & i <= ( len w) holds ex wi be Element of IAlph, qs2i,qs2i1 be State of fsm st wi = (w . i) & qs2i = (qs2 . i) & qs2i1 = (qs2 . (i + 1)) & (wi -succ_of qs2i) = qs2i1;

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len qs1) implies (qs1 . $1) = (qs2 . $1);

         A11:

        now

          let k be Nat;

          assume

           A12: P[k];

          thus P[(k + 1)]

          proof

            assume that 1 <= (k + 1) and

             A13: (k + 1) <= ( len qs1);

            

             A14: 0 = k or 0 < k & ( 0 + 1) = 1;

            per cases by A14, NAT_1: 13;

              suppose 0 = k;

              hence thesis by A5, A8;

            end;

              suppose

               A15: 1 <= k;

              

               A16: k <= ( len w) by A6, A13, XREAL_1: 6;

              then (ex i1 be Element of IAlph, qs1i,qs1i1 be State of fsm st i1 = (w . k) & qs1i = (qs1 . k) & qs1i1 = (qs1 . (k + 1)) & (i1 -succ_of qs1i) = qs1i1) & ex i2 be Element of IAlph, qs2i,qs2i1 be State of fsm st i2 = (w . k) & qs2i = (qs2 . k) & qs2i1 = (qs2 . (k + 1)) & (i2 -succ_of qs2i) = qs2i1 by A7, A10, A15;

              hence thesis by A6, A12, A15, A16, NAT_1: 12;

            end;

          end;

        end;

        

         A17: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A17, A11);

        hence thesis by A6, A9, FINSEQ_1: 14;

      end;

    end

    theorem :: FSM_1:1

    

     Th1: ((q,( <*> IAlph)) -admissible ) = <*q*>

    proof

      set eis = ( <*> IAlph);

      

       A1: for i be Nat st 1 <= i & i <= ( len eis) holds ex wi be Element of IAlph, qi,qi1 be State of fsm st wi = (eis . i) & qi = ( <*q*> . i) & qi1 = ( <*q*> . (i + 1)) & (wi -succ_of qi) = qi1;

      ( len <*q*>) = (( len eis) + 1) & ( <*q*> . 1) = q by FINSEQ_1: 40;

      hence thesis by A1, Def2;

    end;

    definition

      let IAlph be non empty set;

      let fsm be non empty FSM over IAlph;

      let w be FinSequence of IAlph;

      let q1,q2 be State of fsm;

      :: FSM_1:def3

      pred q1,w -leads_to q2 means (((q1,w) -admissible ) . (( len w) + 1)) = q2;

    end

    theorem :: FSM_1:2

    

     Th2: (q,( <*> IAlph)) -leads_to q

    proof

      set eis = ( <*> IAlph);

      

       A1: ( <*q*> . (( len eis) + 1)) = ( <*q*> . ( 0 + 1))

      .= q by FINSEQ_1: 40;

      ((q,eis) -admissible ) = <*q*> by Th1;

      hence thesis by A1;

    end;

    definition

      let IAlph be non empty set;

      let fsm be non empty FSM over IAlph;

      let w be FinSequence of IAlph;

      let qseq be FinSequence of the carrier of fsm;

      :: FSM_1:def4

      pred qseq is_admissible_for w means ex q1 be State of fsm st q1 = (qseq . 1) & ((q1,w) -admissible ) = qseq;

    end

    theorem :: FSM_1:3

     <*q*> is_admissible_for ( <*> IAlph)

    proof

      ((q,( <*> IAlph)) -admissible ) = <*q*> & q = ( <*q*> . 1) by Th1, FINSEQ_1: 40;

      hence thesis;

    end;

    definition

      let IAlph, fsm, q, w;

      :: FSM_1:def5

      func q leads_to_under w -> State of fsm means

      : Def5: (q,w) -leads_to it ;

      existence

      proof

        ( len ((q,w) -admissible )) = (( len w) + 1) & (( len w) + 1) in ( Seg (( len w) + 1)) by Def2, FINSEQ_1: 4;

        then (( len w) + 1) in ( dom ((q,w) -admissible )) by FINSEQ_1:def 3;

        then

        reconsider IT = (((q,w) -admissible ) . (( len w) + 1)) as Element of fsm by FINSEQ_2: 11;

        take IT;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: FSM_1:4

    (((q,w) -admissible ) . ( len ((q,w) -admissible ))) = q9 iff (q,w) -leads_to q9 by Def2;

    theorem :: FSM_1:5

    

     Th5: for k st 1 <= k & k <= ( len w1) holds (((q1,(w1 ^ w2)) -admissible ) . k) = (((q1,w1) -admissible ) . k)

    proof

      set q1w = ((q1,(w1 ^ w2)) -admissible );

      set q1w1 = ((q1,w1) -admissible );

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len w1) implies (q1w . $1) = (q1w1 . $1);

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        thus P[(k + 1)]

        proof

          assume that 1 <= (k + 1) and

           A3: (k + 1) <= ( len w1);

          

           A4: 0 = k or 0 < k & ( 0 + 1) = 1;

          per cases by A3, A4, NAT_1: 13;

            suppose

             A5: k = 0 ;

            

            hence (q1w . (k + 1)) = q1 by Def2

            .= (q1w1 . (k + 1)) by A5, Def2;

          end;

            suppose

             A6: 1 <= k & k <= ( len w1);

            ( len w1) <= (( len w1) + ( len w2)) by NAT_1: 11;

            then k <= (( len w1) + ( len w2)) by A6, XXREAL_0: 2;

            then k <= ( len (w1 ^ w2)) by FINSEQ_1: 22;

            then

             A7: ex wk be Element of IAlph, qwk,qwk1 be State of fsm st wk = ((w1 ^ w2) . k) & qwk = (q1w . k) & qwk1 = (q1w . (k + 1)) & (wk -succ_of qwk) = qwk1 by A6, Def2;

            (ex w1k be Element of IAlph, qw1k,qw1k1 be State of fsm st w1k = (w1 . k) & qw1k = (q1w1 . k) & qw1k1 = (q1w1 . (k + 1)) & (w1k -succ_of qw1k) = qw1k1) & k in ( dom w1) by A6, Def2, FINSEQ_3: 25;

            hence thesis by A2, A6, A7, FINSEQ_1:def 7;

          end;

        end;

      end;

      

       A8: P[ 0 ];

      thus for k be Nat holds P[k] from NAT_1:sch 2( A8, A1);

    end;

    theorem :: FSM_1:6

    

     Th6: (q1,w1) -leads_to q2 implies (((q1,(w1 ^ w2)) -admissible ) . (( len w1) + 1)) = q2

    proof

      assume

       A1: (q1,w1) -leads_to q2;

      set q1w1 = ((q1,w1) -admissible );

      set q1w = ((q1,(w1 ^ w2)) -admissible );

      per cases ;

        suppose

         A2: ( len w1) = 0 ;

        (q1w1 . 1) = q1 & (q1w1 . (( len w1) + 1)) = q2 by A1, Def2;

        hence thesis by A2, Def2;

      end;

        suppose

         A3: ( len w1) > 0 ;

        ( 0 + 1) = 1;

        then

         A4: 1 <= ( len w1) by A3, NAT_1: 13;

        then

        consider w1k be Element of IAlph, qw1k,qw1k1 be State of fsm such that

         A5: w1k = (w1 . ( len w1)) and

         A6: qw1k = (q1w1 . ( len w1)) and

         A7: qw1k1 = (q1w1 . (( len w1) + 1)) and

         A8: (w1k -succ_of qw1k) = qw1k1 by Def2;

        ( len (w1 ^ w2)) = (( len w1) + ( len w2)) by FINSEQ_1: 22;

        then ( len w1) <= ( len (w1 ^ w2)) by NAT_1: 12;

        then

        consider wk be Element of IAlph, qwk,qwk1 be State of fsm such that

         A9: wk = ((w1 ^ w2) . ( len w1)) and

         A10: qwk = (q1w . ( len w1)) & qwk1 = (q1w . (( len w1) + 1)) & (wk -succ_of qwk) = qwk1 by A4, Def2;

        ( len w1) in ( Seg ( len w1)) by A3, FINSEQ_1: 3;

        then ( len w1) in ( dom w1) by FINSEQ_1:def 3;

        then wk = w1k by A9, A5, FINSEQ_1:def 7;

        

        hence (((q1,(w1 ^ w2)) -admissible ) . (( len w1) + 1)) = qw1k1 by A4, A10, A6, A8, Th5

        .= q2 by A1, A7;

      end;

    end;

    theorem :: FSM_1:7

    

     Th7: (q1,w1) -leads_to q2 implies for k st 1 <= k & k <= (( len w2) + 1) holds (((q1,(w1 ^ w2)) -admissible ) . (( len w1) + k)) = (((q2,w2) -admissible ) . k)

    proof

      set q1w = ((q1,(w1 ^ w2)) -admissible );

      set q2w2 = ((q2,w2) -admissible );

      defpred P[ Nat] means 1 <= $1 & $1 <= (( len w2) + 1) implies (q1w . (( len w1) + $1)) = (q2w2 . $1);

      assume

       A1: (q1,w1) -leads_to q2;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: 1 <= k & k <= (( len w2) + 1) implies (q1w . (( len w1) + k)) = (q2w2 . k);

        assume that 1 <= (k + 1) and

         A4: (k + 1) <= (( len w2) + 1);

        per cases ;

          suppose

           A5: k = 0 ;

          

          hence (q1w . (( len w1) + (k + 1))) = q2 by A1, Th6

          .= (q2w2 . (k + 1)) by A5, Def2;

        end;

          suppose

           A6: 0 < k;

          

           A7: k <= ( len w2) by A4, XREAL_1: 6;

          

           A8: ( 0 + 1) = 1;

          then 1 <= k by A6, NAT_1: 13;

          then

           A9: (ex w2i be Element of IAlph, q2i,q2i1 be State of fsm st w2i = (w2 . k) & q2i = (q2w2 . k) & q2i1 = (q2w2 . (k + 1)) & (w2i -succ_of q2i) = q2i1) & k in ( dom w2) by A7, Def2, FINSEQ_3: 25;

          ( len (w1 ^ w2)) = (( len w1) + ( len w2)) by FINSEQ_1: 22;

          then

           A10: (( len w1) + k) <= ( len (w1 ^ w2)) by A7, XREAL_1: 7;

          1 <= (( len w1) + k) by A6, A8, NAT_1: 13;

          then ex wi be Element of IAlph, qi,qi1 be State of fsm st wi = ((w1 ^ w2) . (( len w1) + k)) & qi = (q1w . (( len w1) + k)) & qi1 = (q1w . ((( len w1) + k) + 1)) & (wi -succ_of qi) = qi1 by A10, Def2;

          hence thesis by A3, A4, A6, A8, A9, FINSEQ_1:def 7, NAT_1: 13;

        end;

      end;

      

       A11: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A11, A2);

    end;

    theorem :: FSM_1:8

    

     Th8: (q1,w1) -leads_to q2 implies ((q1,(w1 ^ w2)) -admissible ) = (( Del (((q1,w1) -admissible ),(( len w1) + 1))) ^ ((q2,w2) -admissible ))

    proof

      set q1w = ((q1,(w1 ^ w2)) -admissible );

      set q1w1 = ((q1,w1) -admissible );

      set q2w2 = ((q2,w2) -admissible );

      set Dw1 = ( Del (((q1,w1) -admissible ),(( len w1) + 1)));

      

       A1: ( len q1w1) = (( len w1) + 1) by Def2;

      ( len q1w1) = (( len w1) + 1) & ( dom q1w1) = ( Seg ( len q1w1)) by Def2, FINSEQ_1:def 3;

      then (( len w1) + 1) in ( dom q1w1) by FINSEQ_1: 3;

      then

       A2: ex m be Nat st ( len q1w1) = (m + 1) & ( len Dw1) = m by FINSEQ_3: 104;

      

       A3: ( len q1w) = (( len (w1 ^ w2)) + 1) by Def2

      .= ((( len w1) + ( len w2)) + 1) by FINSEQ_1: 22

      .= (( len Dw1) + (( len w2) + 1)) by A2, A1

      .= (( len Dw1) + ( len q2w2)) by Def2

      .= ( len (Dw1 ^ q2w2)) by FINSEQ_1: 22;

      assume

       A4: (q1,w1) -leads_to q2;

      now

        let k be Nat;

        assume

         A5: 1 <= k & k <= ( len q1w);

        per cases by A5, NAT_1: 13;

          suppose

           A6: 1 <= k & k <= ( len w1);

          then

           A7: k < (( len w1) + 1) by NAT_1: 13;

          

           A8: k in ( dom Dw1) by A2, A1, A6, FINSEQ_3: 25;

          

          thus (q1w . k) = (q1w1 . k) by A6, Th5

          .= (Dw1 . k) by A7, FINSEQ_3: 110

          .= ((Dw1 ^ q2w2) . k) by A8, FINSEQ_1:def 7;

        end;

          suppose

           A9: (( len w1) + 1) <= k & k <= ( len q1w);

          then k <= (( len Dw1) + ( len q2w2)) by A3, FINSEQ_1: 22;

          then

           A10: ((Dw1 ^ q2w2) . k) = (q2w2 . (k - ( len w1))) by A2, A1, A9, FINSEQ_1: 23;

          ((( len w1) + 1) - ( len w1)) <= (k - ( len w1)) by A9, XREAL_1: 9;

          then

          reconsider i = (k - ( len w1)) as Element of NAT by INT_1: 3;

          

           A11: k = (( len w1) + i);

          ( len q1w) = (( len (w1 ^ w2)) + 1) by Def2;

          then k <= ((( len w1) + ( len w2)) + 1) by A9, FINSEQ_1: 22;

          then k <= (( len w1) + (( len w2) + 1));

          then

           A12: i <= (( len w2) + 1) by A11, XREAL_1: 6;

          1 <= i by A9, A11, XREAL_1: 6;

          hence (q1w . k) = ((Dw1 ^ q2w2) . k) by A4, A11, A12, A10, Th7;

        end;

      end;

      hence thesis by A3, FINSEQ_1: 14;

    end;

    begin

    definition

      let IAlph be set, OAlph be non empty set;

      struct ( FSM over IAlph) Mealy-FSM over IAlph,OAlph (# the carrier -> set,

the Tran -> Function of [: the carrier, IAlph:], the carrier,

the OFun -> Function of [: the carrier, IAlph:], OAlph,

the InitS -> Element of the carrier #)

       attr strict strict;

      struct ( FSM over IAlph) Moore-FSM over IAlph,OAlph (# the carrier -> set,

the Tran -> Function of [: the carrier, IAlph:], the carrier,

the OFun -> Function of the carrier, OAlph,

the InitS -> Element of the carrier #)

       attr strict strict;

    end

    registration

      let IAlph be set, X be finite non empty set, T be Function of [:X, IAlph:], X, I be Element of X;

      cluster FSM (# X, T, I #) -> finite non empty;

      coherence ;

    end

    registration

      let IAlph be set, OAlph be non empty set, X be finite non empty set, T be Function of [:X, IAlph:], X, O be Function of [:X, IAlph:], OAlph, I be Element of X;

      cluster Mealy-FSM (# X, T, O, I #) -> finite non empty;

      coherence ;

    end

    registration

      let IAlph be set, OAlph be non empty set, X be finite non empty set, T be Function of [:X, IAlph:], X, O be Function of X, OAlph, I be Element of X;

      cluster Moore-FSM (# X, T, O, I #) -> finite non empty;

      coherence ;

    end

    registration

      let IAlph be set, OAlph be non empty set;

      cluster finite non empty for Mealy-FSM over IAlph, OAlph;

      existence

      proof

        set X = the finite non empty set, T = the Function of [:X, IAlph:], X, O = the Function of [:X, IAlph:], OAlph, I = the Element of X;

        take Mealy-FSM (# X, T, O, I #);

        thus thesis;

      end;

      cluster finite non empty for Moore-FSM over IAlph, OAlph;

      existence

      proof

        set X = the finite non empty set, T = the Function of [:X, IAlph:], X, O = the Function of X, OAlph, I = the Element of X;

        take Moore-FSM (# X, T, O, I #);

        thus thesis;

      end;

    end

    reserve tfsm,tfsm1,tfsm2,tfsm3 for non empty Mealy-FSM over IAlph, OAlph,

sfsm for non empty Moore-FSM over IAlph, OAlph,

qs for State of sfsm,

q,q1,q2,q3,qa,qb,qc,qa9,qt,q1t,q2t for State of tfsm,

q11,q12 for State of tfsm1,

q21,q22 for State of tfsm2;

    definition

      let IAlph, OAlph, tfsm, qt, w;

      :: FSM_1:def6

      func (qt,w) -response -> FinSequence of OAlph means

      : Def6: ( len it ) = ( len w) & for i st i in ( dom w) holds (it . i) = (the OFun of tfsm . [(((qt,w) -admissible ) . i), (w . i)]);

      existence

      proof

        set qs = ((qt,w) -admissible );

        deffunc F( Nat) = (the OFun of tfsm . [(qs . $1), (w . $1)]);

        consider p be FinSequence such that

         A1: ( len p) = ( len w) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

        

         A2: ( Seg ( len w)) = ( dom w) by FINSEQ_1:def 3;

        ( rng p) c= OAlph

        proof

          let y be object;

          assume y in ( rng p);

          then

          consider x be object such that

           A3: x in ( dom p) and

           A4: y = (p . x) by FUNCT_1:def 3;

          reconsider x as Nat by A3;

          x <= ( len p) by A3, FINSEQ_3: 25;

          then

           A5: x <= (( len p) + 1) by NAT_1: 12;

          

           A6: ( len qs) = (( len p) + 1) by A1, Def2;

          ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

          then

          reconsider wx = (w . x) as Element of IAlph by A2, A1, A3, FINSEQ_2: 11;

          1 <= x by A3, FINSEQ_3: 25;

          then x in ( dom qs) by A6, A5, FINSEQ_3: 25;

          then

          reconsider qsx = (qs . x) as Element of tfsm by FINSEQ_2: 11;

          (p . x) = (the OFun of tfsm . [qsx, wx]) by A1, A3;

          hence thesis by A4;

        end;

        then

        reconsider p9 = p as FinSequence of OAlph by FINSEQ_1:def 4;

        ( dom p) = ( dom w) by A1, FINSEQ_3: 29;

        then for i be Nat st i in ( dom w) holds (p9 . i) = (the OFun of tfsm . [(qs . i), (w . i)]) by A1;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of OAlph;

        set qs = ((qt,w) -admissible );

        assume that

         A7: ( len it1) = ( len w) and

         A8: for i be Nat st i in ( dom w) holds (it1 . i) = (the OFun of tfsm . [(qs . i), (w . i)]);

        assume that

         A9: ( len it2) = ( len w) and

         A10: for i be Nat st i in ( dom w) holds (it2 . i) = (the OFun of tfsm . [(qs . i), (w . i)]);

        

         A11: ( dom w) = ( dom it1) by A7, FINSEQ_3: 29;

        now

          thus ( len it1) = ( len it2) by A7, A9;

          let i be Nat;

          assume 1 <= i & i <= ( len it1);

          then

           A12: i in ( dom it1) by FINSEQ_3: 25;

          then (it1 . i) = (the OFun of tfsm . [(qs . i), (w . i)]) by A8, A11;

          hence (it1 . i) = (it2 . i) by A10, A11, A12;

        end;

        hence thesis by FINSEQ_1: 14;

      end;

    end

    theorem :: FSM_1:9

    

     Th9: ((qt,( <*> IAlph)) -response ) = ( <*> OAlph)

    proof

      ( len ((qt,( <*> IAlph)) -response )) = ( len ( <*> IAlph)) by Def6

      .= 0 ;

      hence thesis;

    end;

    definition

      let IAlph, OAlph, sfsm, qs, w;

      :: FSM_1:def7

      func (qs,w) -response -> FinSequence of OAlph means

      : Def7: ( len it ) = (( len w) + 1) & for i st i in ( Seg (( len w) + 1)) holds (it . i) = (the OFun of sfsm . (((qs,w) -admissible ) . i));

      existence

      proof

        set qs9 = ((qs,w) -admissible );

        deffunc F( Nat) = (the OFun of sfsm . (qs9 . $1));

        consider p be FinSequence such that

         A1: ( len p) = ( len qs9) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

        

         A2: ( Seg ( len qs9)) = ( dom qs9) by FINSEQ_1:def 3;

        ( rng p) c= OAlph

        proof

          let y be object;

          assume y in ( rng p);

          then

          consider x be object such that

           A3: x in ( dom p) and

           A4: y = (p . x) by FUNCT_1:def 3;

          reconsider x as Nat by A3;

          ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

          then

          reconsider qsx = (qs9 . x) as State of sfsm by A2, A1, A3, FINSEQ_2: 11;

          (p . x) = (the OFun of sfsm . qsx) by A1, A3;

          hence thesis by A4;

        end;

        then

        reconsider p9 = p as FinSequence of OAlph by FINSEQ_1:def 4;

        

         A5: ( len qs9) = (( len w) + 1) by Def2;

        ( dom p) = ( dom qs9) by A1, FINSEQ_3: 29;

        then for i be Nat st i in ( dom qs9) holds (p9 . i) = (the OFun of sfsm . (qs9 . i)) by A1;

        hence thesis by A2, A1, A5;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of OAlph;

        set qs9 = ((qs,w) -admissible );

        assume that

         A6: ( len it1) = (( len w) + 1) and

         A7: for i be Nat st i in ( Seg (( len w) + 1)) holds (it1 . i) = (the OFun of sfsm . (qs9 . i));

        assume that

         A8: ( len it2) = (( len w) + 1) and

         A9: for i be Nat st i in ( Seg (( len w) + 1)) holds (it2 . i) = (the OFun of sfsm . (qs9 . i));

        now

          thus ( len it1) = ( len it2) by A6, A8;

          let i be Nat;

          assume 1 <= i & i <= ( len it1);

          then

           A10: i in ( Seg ( len it1)) by FINSEQ_1: 1;

          then (it1 . i) = (the OFun of sfsm . (qs9 . i)) by A6, A7;

          hence (it1 . i) = (it2 . i) by A6, A9, A10;

        end;

        hence thesis by FINSEQ_1: 14;

      end;

    end

    theorem :: FSM_1:10

    

     Th10: (((qs,w) -response ) . 1) = (the OFun of sfsm . qs)

    proof

      1 <= (( len w) + 1) by NAT_1: 12;

      then 1 in ( Seg (( len w) + 1)) by FINSEQ_1: 1;

      

      hence (((qs,w) -response ) . 1) = (the OFun of sfsm . (((qs,w) -admissible ) . 1)) by Def7

      .= (the OFun of sfsm . qs) by Def2;

    end;

    theorem :: FSM_1:11

    

     Th11: (q1t,w1) -leads_to q2t implies ((q1t,(w1 ^ w2)) -response ) = (((q1t,w1) -response ) ^ ((q2t,w2) -response ))

    proof

      set q1w1 = ((q1t,w1) -response ), q2w2 = ((q2t,w2) -response );

      set q1w1w2 = ((q1t,(w1 ^ w2)) -response );

      set Dq1w1w2a = ( Del (((q1t,w1) -admissible ),(( len w1) + 1)));

      set OF = the OFun of tfsm;

      assume

       A1: (q1t,w1) -leads_to q2t;

       A2:

      now

        ( dom ((q1t,w1) -admissible )) = ( Seg ( len ((q1t,w1) -admissible ))) by FINSEQ_1:def 3;

        then ( dom ((q1t,w1) -admissible )) = ( Seg (( len w1) + 1)) by Def2;

        then (( len w1) + 1) in ( dom ((q1t,w1) -admissible )) by FINSEQ_1: 3;

        then

        consider m be Nat such that

         A3: ( len ((q1t,w1) -admissible )) = (m + 1) and

         A4: ( len Dq1w1w2a) = m by FINSEQ_3: 104;

        

         A5: (m + 1) = (( len w1) + 1) by A3, Def2;

        

         A6: ( len q1w1) = ( len w1) by Def6;

        let k be Nat;

        assume that

         A7: 1 <= k and

         A8: k <= ( len q1w1w2);

        per cases by A7, A8, NAT_1: 13;

          suppose

           A9: 1 <= k & k <= ( len q1w1);

          then

           A10: k <= ( len w1) by Def6;

          then

           A11: k in ( dom w1) by A9, FINSEQ_3: 25;

          

           A12: k in ( dom Dq1w1w2a) by A4, A5, A9, A10, FINSEQ_3: 25;

          

           A13: k < (( len w1) + 1) by A10, NAT_1: 13;

          

           A14: k in ( dom q1w1) by A9, FINSEQ_3: 25;

          k <= ( len (w1 ^ w2)) by A8, Def6;

          then k in ( dom (w1 ^ w2)) by A7, FINSEQ_3: 25;

          

          hence (q1w1w2 . k) = (OF . [(((q1t,(w1 ^ w2)) -admissible ) . k), ((w1 ^ w2) . k)]) by Def6

          .= (OF . [((Dq1w1w2a ^ ((q2t,w2) -admissible )) . k), ((w1 ^ w2) . k)]) by A1, Th8

          .= (OF . [(Dq1w1w2a . k), ((w1 ^ w2) . k)]) by A12, FINSEQ_1:def 7

          .= (OF . [(Dq1w1w2a . k), (w1 . k)]) by A11, FINSEQ_1:def 7

          .= (OF . [(((q1t,w1) -admissible ) . k), (w1 . k)]) by A13, FINSEQ_3: 110

          .= (((q1t,w1) -response ) . k) by A11, Def6

          .= ((((q1t,w1) -response ) ^ ((q2t,w2) -response )) . k) by A14, FINSEQ_1:def 7;

        end;

          suppose

           A15: (( len q1w1) + 1) <= k & k <= ( len q1w1w2);

          then

           A16: ((( len q1w1) + 1) - ( len q1w1)) <= (k - ( len q1w1)) by XREAL_1: 9;

          then

          reconsider p = (k - ( len q1w1)) as Element of NAT by INT_1: 3;

          

           A17: ( len q1w1w2) = ( len (w1 ^ w2)) by Def6

          .= (( len w1) + ( len w2)) by FINSEQ_1: 22;

          then k <= (( len q1w1) + ( len w2)) by A15, Def6;

          then (k - ( len q1w1)) <= ((( len q1w1) + ( len w2)) - ( len q1w1)) by XREAL_1: 9;

          then

           A18: p in ( dom w2) by A16, FINSEQ_3: 25;

          

           A19: (( len Dq1w1w2a) + 1) <= k by A4, A5, A15, Def6;

          

           A20: (( len w1) + 1) <= k by A15, Def6;

          

           A21: ( len q1w1w2) = ( len (w1 ^ w2)) by Def6

          .= (( len w1) + ( len w2)) by FINSEQ_1: 22

          .= (( len q1w1) + ( len w2)) by Def6

          .= (( len q1w1) + ( len q2w2)) by Def6;

          

          then

           A22: ((q1w1 ^ q2w2) . k) = (((q2t,w2) -response ) . p) by A15, FINSEQ_1: 23

          .= (OF . [(((q2t,w2) -admissible ) . p), (w2 . p)]) by A18, Def6

          .= (OF . [(((q2t,w2) -admissible ) . (k - ( len w1))), (w2 . (k - ( len q1w1)))]) by Def6

          .= (OF . [(((q2t,w2) -admissible ) . (k - ( len w1))), (w2 . (k - ( len w1)))]) by Def6;

          ( len w2) <= (( len w2) + 1) by NAT_1: 11;

          then

           A23: (( len Dq1w1w2a) + ( len w2)) <= (( len Dq1w1w2a) + (( len w2) + 1)) by XREAL_1: 6;

          k <= (( len Dq1w1w2a) + ( len w2)) by A4, A5, A6, A15, A21, Def6;

          then k <= (( len Dq1w1w2a) + (( len w2) + 1)) by A23, XXREAL_0: 2;

          then

           A24: k <= (( len Dq1w1w2a) + ( len ((q2t,w2) -admissible ))) by Def2;

          k <= ( len (w1 ^ w2)) by A8, Def6;

          then k in ( dom (w1 ^ w2)) by A7, FINSEQ_3: 25;

          

          then (q1w1w2 . k) = (OF . [(((q1t,(w1 ^ w2)) -admissible ) . k), ((w1 ^ w2) . k)]) by Def6

          .= (OF . [((( Del (((q1t,w1) -admissible ),(( len w1) + 1))) ^ ((q2t,w2) -admissible )) . k), ((w1 ^ w2) . k)]) by A1, Th8

          .= (OF . [(((q2t,w2) -admissible ) . (k - ( len Dq1w1w2a))), ((w1 ^ w2) . k)]) by A19, A24, FINSEQ_1: 23

          .= (OF . [(((q2t,w2) -admissible ) . (k - ( len w1))), (w2 . (k - ( len w1)))]) by A4, A5, A15, A17, A20, FINSEQ_1: 23;

          hence (q1w1w2 . k) = ((q1w1 ^ q2w2) . k) by A22;

        end;

      end;

      ( len q1w1w2) = ( len (w1 ^ w2)) by Def6

      .= (( len w1) + ( len w2)) by FINSEQ_1: 22

      .= (( len q1w1) + ( len w2)) by Def6

      .= (( len q1w1) + ( len q2w2)) by Def6

      .= ( len (q1w1 ^ q2w2)) by FINSEQ_1: 22;

      hence thesis by A2, FINSEQ_1: 14;

    end;

    theorem :: FSM_1:12

    

     Th12: (q11,w1) -leads_to q12 & (q21,w1) -leads_to q22 & ((q12,w2) -response ) <> ((q22,w2) -response ) implies ((q11,(w1 ^ w2)) -response ) <> ((q21,(w1 ^ w2)) -response )

    proof

      assume that

       A1: (q11,w1) -leads_to q12 and

       A2: (q21,w1) -leads_to q22 and

       A3: ((q12,w2) -response ) <> ((q22,w2) -response );

      set r12 = ((q12,w2) -response ), r22 = ((q22,w2) -response );

      

       A4: ( len r22) = ( len w2) by Def6;

      set w = (w1 ^ w2);

      set r1w1 = ((q11,w1) -response ), r2w1 = ((q21,w1) -response );

      assume

       A5: ((q11,(w1 ^ w2)) -response ) = ((q21,(w1 ^ w2)) -response );

      set r21 = ((q21,w) -response );

      

       A6: r21 = (r2w1 ^ r22) by A2, Th11;

      set r11 = ((q11,w) -response );

      

       A7: r11 = (r1w1 ^ r12) by A1, Th11;

      

       A8: ( len r1w1) = ( len w1) by Def6;

      

       A9: ( len r12) = ( len w2) by Def6;

      then

       A10: ( dom w2) = ( Seg ( len r12)) by FINSEQ_1:def 3;

      then ( dom w2) = ( dom r12) by FINSEQ_1:def 3;

      then

      consider j be Nat such that

       A11: j in ( dom w2) and

       A12: (r12 . j) <> (r22 . j) by A3, A9, A4, FINSEQ_2: 9;

      

       A13: ( len r2w1) = ( len w1) by Def6;

      j in ( dom r12) by A10, A11, FINSEQ_1:def 3;

      then

       A14: (r11 . (( len w1) + j)) = (r12 . j) by A8, A7, FINSEQ_1:def 7;

      j in ( dom r22) by A9, A4, A10, A11, FINSEQ_1:def 3;

      hence contradiction by A5, A13, A12, A6, A14, FINSEQ_1:def 7;

    end;

    reserve OAlphf for finite non empty set,

tfsmf for finite non empty Mealy-FSM over IAlph, OAlphf,

sfsmf for finite non empty Moore-FSM over IAlph, OAlphf;

    definition

      let IAlph, OAlph;

      let tfsm be non empty Mealy-FSM over IAlph, OAlph;

      let sfsm be non empty Moore-FSM over IAlph, OAlph;

      :: FSM_1:def8

      pred tfsm is_similar_to sfsm means for tw be FinSequence of IAlph holds ( <*(the OFun of sfsm . the InitS of sfsm)*> ^ ((the InitS of tfsm,tw) -response )) = ((the InitS of sfsm,tw) -response );

    end

    theorem :: FSM_1:13

    for sfsm be non empty finite Moore-FSM over IAlph, OAlph holds ex tfsm be non empty finite Mealy-FSM over IAlph, OAlph st tfsm is_similar_to sfsm

    proof

      let sfsm be non empty finite Moore-FSM over IAlph, OAlph;

      set S = the carrier of sfsm, T = the Tran of sfsm;

      set sOF = the OFun of sfsm, IS = the InitS of sfsm;

      deffunc F( Element of S, Element of IAlph) = (sOF . (T . [$1, $2]));

      consider tOF be Function of [:S, IAlph:], OAlph such that

       A1: for q be Element of S, s be Element of IAlph holds (tOF . (q,s)) = F(q,s) from BINOP_1:sch 4;

      take tfsm = Mealy-FSM (# S, T, tOF, IS #);

      let tw be FinSequence of IAlph;

      set tIS = the InitS of tfsm;

      set twa = ((tIS,tw) -admissible );

      set swa = ((IS,tw) -admissible );

      defpred P[ Nat] means $1 in ( Seg (( len tw) + 1)) implies (twa . $1) = (swa . $1);

      

       A2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: i in ( Seg (( len tw) + 1)) implies (twa . i) = (swa . i);

        assume (i + 1) in ( Seg (( len tw) + 1));

        then

         A4: (i + 1) <= (( len tw) + 1) by FINSEQ_1: 1;

        per cases by A4, XREAL_1: 6;

          suppose

           A5: i = 0 ;

          (twa . 1) = the InitS of tfsm by Def2;

          hence thesis by A5, Def2;

        end;

          suppose

           A6: i > 0 & i <= ( len tw);

          then

           A7: i <= (( len tw) + 1) by NAT_1: 13;

          

           A8: ( 0 + 1) = 1 implies 1 <= i & i <= ( len tw) by A6, NAT_1: 13;

          then (ex twi be Element of IAlph, tqi,tqi1 be Element of tfsm st twi = (tw . i) & tqi = (twa . i) & tqi1 = (twa . (i + 1)) & (twi -succ_of tqi) = tqi1) & ex swi be Element of IAlph, sqi,sqi1 be Element of sfsm st swi = (tw . i) & sqi = (swa . i) & sqi1 = (swa . (i + 1)) & (swi -succ_of sqi) = sqi1 by Def2;

          hence thesis by A3, A8, A7, FINSEQ_1: 1;

        end;

      end;

      

       A9: P[ 0 ] by FINSEQ_1: 1;

      

       A10: for i be Nat holds P[i] from NAT_1:sch 2( A9, A2);

      now

        

        thus ( len ( <*(sOF . IS)*> ^ ((tIS,tw) -response ))) = (( len <*(sOF . IS)*>) + ( len ((tIS,tw) -response ))) by FINSEQ_1: 22

        .= (1 + ( len ((tIS,tw) -response ))) by FINSEQ_1: 40

        .= (( len tw) + 1) by Def6;

        then

         A11: ( dom ( <*(sOF . IS)*> ^ ((tIS,tw) -response ))) = ( Seg (( len tw) + 1)) by FINSEQ_1:def 3;

        thus ( len ((IS,tw) -response )) = (( len tw) + 1) by Def7;

        let i be Nat;

        assume

         A12: i in ( dom ( <*(sOF . IS)*> ^ ((tIS,tw) -response )));

        then

         A13: 1 <= i by A11, FINSEQ_1: 1;

        

         A14: i <= (( len tw) + 1) by A11, A12, FINSEQ_1: 1;

        per cases by A13, XXREAL_0: 1;

          suppose

           A15: i = 1;

          then i in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

          then i in ( dom <*(sOF . IS)*>) by FINSEQ_1: 38;

          

          hence (( <*(sOF . IS)*> ^ ((tIS,tw) -response )) . i) = ( <*(sOF . IS)*> . i) by FINSEQ_1:def 7

          .= (sOF . IS) by A15, FINSEQ_1: 40

          .= (((IS,tw) -response ) . i) by A15, Th10;

        end;

          suppose 1 < i;

          then

          consider j be Element of NAT such that

           A16: j = (i - 1) and

           A17: 1 <= j by INT_1: 51;

          

           A18: i = (j + 1) by A16;

          then

           A19: j <= ( len tw) by A14, XREAL_1: 6;

          then

          consider swj be Element of IAlph, swaj,swai be Element of sfsm such that

           A20: swj = (tw . j) & swaj = (swa . j) and

           A21: swai = (swa . (j + 1)) & (swj -succ_of swaj) = swai by A17, Def2;

          

           A22: j in ( Seg ( len tw)) by A17, A19, FINSEQ_1: 1;

          then

           A23: j in ( dom tw) by FINSEQ_1:def 3;

          j <= (( len tw) + 1) by A19, NAT_1: 12;

          then

           A24: j in ( Seg (( len tw) + 1)) by A17, FINSEQ_1: 1;

          ( len ((tIS,tw) -response )) = ( len tw) by Def6;

          then ( len <*(sOF . IS)*>) = 1 & j in ( dom ((tIS,tw) -response )) by A22, FINSEQ_1: 40, FINSEQ_1:def 3;

          

          then (( <*(sOF . IS)*> ^ ((tIS,tw) -response )) . i) = (((tIS,tw) -response ) . j) by A18, FINSEQ_1:def 7

          .= (the OFun of tfsm . [(((tIS,tw) -admissible ) . j), (tw . j)]) by A23, Def6

          .= (tOF . ((((IS,tw) -admissible ) . j),(tw . j))) by A10, A24

          .= (sOF . (T . (swaj,swj))) by A1, A20

          .= (((IS,tw) -response ) . i) by A11, A12, A16, A21, Def7;

          hence (( <*(sOF . IS)*> ^ ((tIS,tw) -response )) . i) = (((IS,tw) -response ) . i);

        end;

      end;

      hence thesis by FINSEQ_2: 9;

    end;

    theorem :: FSM_1:14

    ex sfsmf st tfsmf is_similar_to sfsmf

    proof

      set S = the carrier of tfsmf, T = the Tran of tfsmf;

      set tOF = the OFun of tfsmf, IS = the InitS of tfsmf;

      set sS = [:S, OAlphf:];

      deffunc F( Element of sS, Element of IAlph) = [(T . [($1 `1 ), $2]), (tOF . [($1 `1 ), $2])];

      consider sT be Function of [:sS, IAlph:], sS such that

       A1: for q be Element of sS, s be Element of IAlph holds (sT . (q,s)) = F(q,s) from BINOP_1:sch 4;

      set sSs = sS, sTs = sT;

      set r0 = the Element of OAlphf;

      deffunc F( Element of S, Element of OAlphf) = $2;

      consider sOF be Function of sS, OAlphf such that

       A2: for q be Element of S, r be Element of OAlphf holds (sOF . (q,r)) = F(q,r) from BINOP_1:sch 4;

      set sI = [IS, r0];

      reconsider sOFs = sOF as Function of sSs, OAlphf;

      reconsider sfsmf = Moore-FSM (# sSs, sTs, sOFs, sI #) as finite non empty Moore-FSM over IAlph, OAlphf;

      take sfsmf;

      reconsider SI = sI as Element of sfsmf;

      thus tfsmf is_similar_to sfsmf

      proof

        let tw be FinSequence of IAlph;

        set twa = ((the InitS of tfsmf,tw) -admissible );

        set swa = ((the InitS of sfsmf,tw) -admissible );

        defpred P[ Nat] means $1 in ( Seg (( len tw) + 1)) implies (twa . $1) = ((swa . $1) `1 );

        

         A3: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat;

          assume

           A4: P[i];

          assume (i + 1) in ( Seg (( len tw) + 1));

          then

           A5: (i + 1) <= (( len tw) + 1) by FINSEQ_1: 1;

          per cases by A5, XREAL_1: 6;

            suppose

             A6: i = 0 ;

            (twa . 1) = IS by Def2

            .= ( [IS, r0] `1 )

            .= ((swa . 1) `1 ) by Def2;

            hence thesis by A6;

          end;

            suppose

             A7: i > 0 & i <= ( len tw);

            then

             A8: i <= (( len tw) + 1) by NAT_1: 13;

            

             A9: ( 0 + 1) = 1 implies 1 <= i & i <= ( len tw) by A7, NAT_1: 13;

            then

             A10: ex twi be Element of IAlph, tqi,tqi1 be Element of tfsmf st twi = (tw . i) & tqi = (twa . i) & tqi1 = (twa . (i + 1)) & (twi -succ_of tqi) = tqi1 by Def2;

            consider swi be Element of IAlph, sqi,sqi1 be Element of sfsmf such that

             A11: swi = (tw . i) & sqi = (swa . i) & sqi1 = (swa . (i + 1)) and

             A12: (swi -succ_of sqi) = sqi1 by A9, Def2;

            sqi1 = (sT . (sqi,swi)) by A12

            .= [(T . [(sqi `1 ), swi]), (tOF . [(sqi `1 ), swi])] by A1;

            hence thesis by A4, A9, A8, A10, A11, FINSEQ_1: 1;

          end;

        end;

        

         A13: P[ 0 ] by FINSEQ_1: 1;

        

         A14: for i be Nat holds P[i] from NAT_1:sch 2( A13, A3);

        now

          

          thus ( len ( <*(sOF . sI)*> ^ ((IS,tw) -response ))) = (( len <*(sOF . sI)*>) + ( len ((IS,tw) -response ))) by FINSEQ_1: 22

          .= (1 + ( len ((IS,tw) -response ))) by FINSEQ_1: 40

          .= (( len tw) + 1) by Def6;

          then

           A15: ( dom ( <*(sOF . sI)*> ^ ((IS,tw) -response ))) = ( Seg (( len tw) + 1)) by FINSEQ_1:def 3;

          thus ( len ((SI,tw) -response )) = (( len tw) + 1) by Def7;

          let i be Nat;

          assume

           A16: i in ( dom ( <*(sOF . sI)*> ^ ((IS,tw) -response )));

          then

           A17: 1 <= i by A15, FINSEQ_1: 1;

          

           A18: i <= (( len tw) + 1) by A15, A16, FINSEQ_1: 1;

          per cases by A17, XXREAL_0: 1;

            suppose

             A19: i = 1;

            then i in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

            then i in ( dom <*(sOF . sI)*>) by FINSEQ_1: 38;

            

            hence (( <*(sOF . sI)*> ^ ((IS,tw) -response )) . i) = ( <*(sOF . sI)*> . i) by FINSEQ_1:def 7

            .= (sOF . sI) by A19, FINSEQ_1: 40

            .= (((SI,tw) -response ) . i) by A19, Th10;

          end;

            suppose 1 < i;

            then

            consider j be Element of NAT such that

             A20: j = (i - 1) and

             A21: 1 <= j by INT_1: 51;

            

             A22: i = (j + 1) by A20;

            then

             A23: j <= ( len tw) by A18, XREAL_1: 6;

            then

            consider swj be Element of IAlph, swaj,swai be Element of sfsmf such that

             A24: swj = (tw . j) and

             A25: swaj = (swa . j) and

             A26: swai = (swa . (j + 1)) & (swj -succ_of swaj) = swai by A21, Def2;

            j <= (( len tw) + 1) by A23, NAT_1: 12;

            then

             A27: j in ( Seg (( len tw) + 1)) by A21, FINSEQ_1: 1;

            reconsider swaj as Element of sS;

            

             A28: j in ( Seg ( len tw)) by A21, A23, FINSEQ_1: 1;

            then

             A29: j in ( dom tw) by FINSEQ_1:def 3;

            ( len ((IS,tw) -response )) = ( len tw) by Def6;

            then ( len <*(sOF . sI)*>) = 1 & j in ( dom ((IS,tw) -response )) by A28, FINSEQ_1: 40, FINSEQ_1:def 3;

            

            hence (( <*(sOF . sI)*> ^ ((IS,tw) -response )) . i) = (((IS,tw) -response ) . j) by A22, FINSEQ_1:def 7

            .= (tOF . ((((IS,tw) -admissible ) . j),(tw . j))) by A29, Def6

            .= (tOF . ((swaj `1 ),(tw . j))) by A14, A27, A25

            .= (sOF . ((T . ((swaj `1 ),swj)),(tOF . ((swaj `1 ),swj)))) by A2, A24

            .= (sOF . (sT . (swaj,swj))) by A1

            .= (((SI,tw) -response ) . i) by A15, A16, A20, A26, Def7;

          end;

        end;

        hence thesis by FINSEQ_2: 9;

      end;

    end;

    begin

    definition

      let IAlph,OAlph be non empty set, tfsm1,tfsm2 be non empty Mealy-FSM over IAlph, OAlph;

      :: FSM_1:def9

      pred tfsm1,tfsm2 -are_equivalent means for w be FinSequence of IAlph holds ((the InitS of tfsm1,w) -response ) = ((the InitS of tfsm2,w) -response );

      reflexivity ;

      symmetry ;

    end

    theorem :: FSM_1:15

    

     Th15: (tfsm1,tfsm2) -are_equivalent & (tfsm2,tfsm3) -are_equivalent implies (tfsm1,tfsm3) -are_equivalent

    proof

      assume that

       A1: (tfsm1,tfsm2) -are_equivalent and

       A2: (tfsm2,tfsm3) -are_equivalent ;

      let w1 be FinSequence of IAlph;

      set IS3 = the InitS of tfsm3;

      set IS1 = the InitS of tfsm1, IS2 = the InitS of tfsm2;

      

      thus ((IS1,w1) -response ) = ((IS2,w1) -response ) by A1

      .= ((IS3,w1) -response ) by A2;

    end;

    definition

      let IAlph, OAlph, tfsm, qa, qb;

      :: FSM_1:def10

      pred qa,qb -are_equivalent means for w holds ((qa,w) -response ) = ((qb,w) -response );

      reflexivity ;

      symmetry ;

    end

    theorem :: FSM_1:16

    (q1,q2) -are_equivalent & (q2,q3) -are_equivalent implies (q1,q3) -are_equivalent

    proof

      assume that

       A1: (q1,q2) -are_equivalent and

       A2: (q2,q3) -are_equivalent ;

      thus (q1,q3) -are_equivalent

      proof

        let w be FinSequence of IAlph;

        ((q1,w) -response ) = ((q2,w) -response ) by A1;

        hence thesis by A2;

      end;

    end;

    theorem :: FSM_1:17

    

     Th17: qa9 = (the Tran of tfsm . [qa, s]) implies for i st i in ( Seg (( len w) + 1)) holds (((qa,( <*s*> ^ w)) -admissible ) . (i + 1)) = (((qa9,w) -admissible ) . i)

    proof

      set sw = ( <*s*> ^ w);

      

       A1: ( len sw) = (( len <*s*>) + ( len w)) by FINSEQ_1: 22

      .= (( len w) + 1) by FINSEQ_1: 40;

      defpred P[ Nat] means $1 in ( Seg (( len w) + 1)) implies (((qa,( <*s*> ^ w)) -admissible ) . ($1 + 1)) = (((qa9,w) -admissible ) . $1);

      

       A2: (sw . 1) = s by FINSEQ_1: 41;

      assume

       A3: qa9 = (the Tran of tfsm . [qa, s]);

      

       A4: for j be Nat st P[j] holds P[(j + 1)]

      proof

        let j be Nat;

        assume

         A5: j in ( Seg (( len w) + 1)) implies (((qa,( <*s*> ^ w)) -admissible ) . (j + 1)) = (((qa9,w) -admissible ) . j);

        assume

         A6: (j + 1) in ( Seg (( len w) + 1));

        per cases ;

          suppose

           A7: j = 0 ;

          set aadm = ((qa,sw) -admissible );

          1 <= ( len sw) by A1, A6, A7, FINSEQ_1: 1;

          then

           A8: ex swi1 be Element of IAlph, a1,a11 be Element of tfsm st swi1 = (sw . 1) & a1 = (aadm . 1) & a11 = (aadm . (1 + 1)) & (swi1 -succ_of a1) = a11 by Def2;

          (((qa9,w) -admissible ) . 1) = qa9 by Def2;

          hence thesis by A3, A2, A7, A8, Def2;

        end;

          suppose

           A9: j <> 0 ;

          set aadm = ((qa,sw) -admissible ), aadm9 = ((qa9,w) -admissible );

          

           A10: j in ( Seg ( len w)) by A6, A9, FINSEQ_1: 61;

          then

           A11: j <= ( len w) by FINSEQ_1: 1;

          then 1 <= (j + 1) & (j + 1) <= ( len sw) by A1, NAT_1: 12, XREAL_1: 7;

          then

           A12: ex swj1 be Element of IAlph, aj1,aj11 be Element of tfsm st swj1 = (sw . (j + 1)) & aj1 = (aadm . (j + 1)) & aj11 = (aadm . ((j + 1) + 1)) & (swj1 -succ_of aj1) = aj11 by Def2;

          1 <= j by A10, FINSEQ_1: 1;

          then

           A13: ex wj be Element of IAlph, aj9,aj19 be Element of tfsm st wj = (w . j) & aj9 = (aadm9 . j) & aj19 = (aadm9 . (j + 1)) & (wj -succ_of aj9) = aj19 by A11, Def2;

          j in ( dom w) by A10, FINSEQ_1:def 3;

          hence thesis by A5, A6, A9, A12, A13, FINSEQ_1: 61, FINSEQ_3: 103;

        end;

      end;

      

       A14: P[ 0 ] by FINSEQ_1: 1;

      thus for i be Nat holds P[i] from NAT_1:sch 2( A14, A4);

    end;

    theorem :: FSM_1:18

    

     Th18: qa9 = (the Tran of tfsm . [qa, s]) implies ((qa,( <*s*> ^ w)) -response ) = ( <*(the OFun of tfsm . [qa, s])*> ^ ((qa9,w) -response ))

    proof

      set OF = the OFun of tfsm;

      set asresp = (OF . [qa, s]);

      

       A1: ( len ( <*s*> ^ w)) = (( len <*s*>) + ( len w)) by FINSEQ_1: 22

      .= (1 + ( len w)) by FINSEQ_1: 40;

      assume

       A2: qa9 = (the Tran of tfsm . [qa, s]);

      now

        thus ( len ((qa,( <*s*> ^ w)) -response )) = (1 + ( len w)) by A1, Def6;

        then

         A3: ( dom ((qa,( <*s*> ^ w)) -response )) = ( Seg (1 + ( len w))) by FINSEQ_1:def 3;

        

        thus

         A4: ( len ( <*asresp*> ^ ((qa9,w) -response ))) = (( len <*asresp*>) + ( len ((qa9,w) -response ))) by FINSEQ_1: 22

        .= (1 + ( len ((qa9,w) -response ))) by FINSEQ_1: 40

        .= (1 + ( len w)) by Def6;

        let j be Nat;

        assume

         A5: j in ( dom ((qa,( <*s*> ^ w)) -response ));

        then

         A6: 1 <= j by A3, FINSEQ_1: 1;

        

         A7: j <= (1 + ( len w)) by A3, A5, FINSEQ_1: 1;

        

         A8: j in ( dom ( <*s*> ^ w)) by A1, A3, A5, FINSEQ_1:def 3;

        per cases by A6, XXREAL_0: 1;

          suppose

           A9: j = 1;

          

          thus (((qa,( <*s*> ^ w)) -response ) . j) = (OF . [(((qa,( <*s*> ^ w)) -admissible ) . j), (( <*s*> ^ w) . j)]) by A8, Def6

          .= (OF . [qa, (( <*s*> ^ w) . j)]) by A9, Def2

          .= asresp by A9, FINSEQ_1: 41

          .= (( <*asresp*> ^ ((qa9,w) -response )) . j) by A9, FINSEQ_1: 41;

        end;

          suppose

           A10: j > 1;

          then

          consider i be Element of NAT such that

           A11: i = (j - 1) and

           A12: 1 <= i by INT_1: 51;

          j <= (( len w) + 1) by A3, A5, FINSEQ_1: 1;

          then (j - 1) <= ((( len w) + 1) - 1) by XREAL_1: 9;

          then

           A13: i in ( Seg ( len w)) by A11, A12, FINSEQ_1: 1;

          then

           A14: i in ( Seg (1 + ( len w))) by FINSEQ_2: 8;

          (i + 1) in ( Seg (1 + ( len w))) by A13, FINSEQ_1: 60;

          then

           A15: (i + 1) in ( dom ( <*s*> ^ w)) by A1, FINSEQ_1:def 3;

          

           A16: i in ( dom w) by A13, FINSEQ_1:def 3;

          ( len <*asresp*>) = 1 by FINSEQ_1: 40;

          

          then (( <*asresp*> ^ ((qa9,w) -response )) . j) = (((qa9,w) -response ) . i) by A4, A7, A10, A11, FINSEQ_1: 24

          .= (OF . [(((qa9,w) -admissible ) . i), (w . i)]) by A16, Def6

          .= (OF . [(((qa9,w) -admissible ) . i), (( <*s*> ^ w) . (i + 1))]) by A16, FINSEQ_3: 103

          .= (OF . [(((qa,( <*s*> ^ w)) -admissible ) . (i + 1)), (( <*s*> ^ w) . (i + 1))]) by A2, A14, Th17

          .= (((qa,( <*s*> ^ w)) -response ) . j) by A11, A15, Def6;

          hence (((qa,( <*s*> ^ w)) -response ) . j) = (( <*asresp*> ^ ((qa9,w) -response )) . j);

        end;

      end;

      hence thesis by FINSEQ_2: 9;

    end;

    theorem :: FSM_1:19

    

     Th19: (qa,qb) -are_equivalent iff for s holds (the OFun of tfsm . [qa, s]) = (the OFun of tfsm . [qb, s]) & ((the Tran of tfsm . [qa, s]),(the Tran of tfsm . [qb, s])) -are_equivalent

    proof

      set OF = the OFun of tfsm;

      hereby

        assume

         A1: (qa,qb) -are_equivalent ;

        let s be Element of IAlph;

        set qa9 = (the Tran of tfsm . [qa, s]);

        set qb9 = (the Tran of tfsm . [qb, s]);

        ( len <*s*>) = 1 by FINSEQ_1: 40;

        then

         A2: 1 in ( dom <*s*>) by FINSEQ_3: 25;

        

        thus

         A3: (OF . [qa, s]) = (OF . [(((qa, <*s*>) -admissible ) . 1), s]) by Def2

        .= (OF . [(((qa, <*s*>) -admissible ) . 1), ( <*s*> . 1)]) by FINSEQ_1: 40

        .= (((qa, <*s*>) -response ) . 1) by A2, Def6

        .= (((qb, <*s*>) -response ) . 1) by A1

        .= (OF . [(((qb, <*s*>) -admissible ) . 1), ( <*s*> . 1)]) by A2, Def6

        .= (OF . [(((qb, <*s*>) -admissible ) . 1), s]) by FINSEQ_1: 40

        .= (OF . [qb, s]) by Def2;

        now

          let w be FinSequence of IAlph;

          

           A4: ((qa,( <*s*> ^ w)) -response ) = ( <*(OF . [qa, s])*> ^ ((qa9,w) -response )) & ((qb,( <*s*> ^ w)) -response ) = ( <*(OF . [qb, s])*> ^ ((qb9,w) -response )) by Th18;

          ((qa,( <*s*> ^ w)) -response ) = ((qb,( <*s*> ^ w)) -response ) by A1;

          hence ((qa9,w) -response ) = ((qb9,w) -response ) by A3, A4, FINSEQ_1: 33;

        end;

        hence ((the Tran of tfsm . [qa, s]),(the Tran of tfsm . [qb, s])) -are_equivalent ;

      end;

      assume

       A5: for s be Element of IAlph holds (the OFun of tfsm . [qa, s]) = (the OFun of tfsm . [qb, s]) & ((the Tran of tfsm . [qa, s]),(the Tran of tfsm . [qb, s])) -are_equivalent ;

      let w be FinSequence of IAlph;

      per cases ;

        suppose

         A6: w = ( <*> IAlph);

        

        hence ((qa,w) -response ) = ( <*> OAlph) by Th9

        .= ((qb,w) -response ) by A6, Th9;

      end;

        suppose w <> {} ;

        then

        consider s be Element of IAlph, wt be FinSequence of IAlph such that s = (w . 1) and

         A7: w = ( <*s*> ^ wt) by FINSEQ_3: 102;

        set bsresp = (the OFun of tfsm . [qb, s]);

        set asresp = (the OFun of tfsm . [qa, s]);

        set qb9 = (the Tran of tfsm . [qb, s]);

        set qa9 = (the Tran of tfsm . [qa, s]);

        (qa9,qb9) -are_equivalent by A5;

        then

         A8: ((qa9,wt) -response ) = ((qb9,wt) -response );

        

        thus ((qa,w) -response ) = ( <*asresp*> ^ ((qa9,wt) -response )) by A7, Th18

        .= ( <*bsresp*> ^ ((qb9,wt) -response )) by A5, A8

        .= ((qb,w) -response ) by A7, Th18;

      end;

    end;

    theorem :: FSM_1:20

    (qa,qb) -are_equivalent implies for w, i st i in ( dom w) holds ex qai,qbi be State of tfsm st qai = (((qa,w) -admissible ) . i) & qbi = (((qb,w) -admissible ) . i) & (qai,qbi) -are_equivalent

    proof

      assume

       A1: (qa,qb) -are_equivalent ;

      let w be FinSequence of IAlph;

      defpred P[ Nat] means $1 in ( Seg ( len w)) implies ex qai,qbi be Element of tfsm st qai = (((qa,w) -admissible ) . $1) & qbi = (((qb,w) -admissible ) . $1) & (qai,qbi) -are_equivalent ;

      

       A2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A3: i in ( Seg ( len w)) implies ex qai,qbi be Element of tfsm st qai = (((qa,w) -admissible ) . i) & qbi = (((qb,w) -admissible ) . i) & (qai,qbi) -are_equivalent ;

        

         A4: i = 0 or 0 < i & ( 0 + 1) = 1;

        assume (i + 1) in ( Seg ( len w));

        then (i + 1) <= ( len w) by FINSEQ_1: 1;

        then

         A5: 0 = i or 1 <= i & i <= ( len w) by A4, NAT_1: 13;

        per cases by A5, FINSEQ_1: 1;

          suppose

           A6: i = 0 ;

          reconsider qai = (((qa,w) -admissible ) . 1), qbi = (((qb,w) -admissible ) . 1) as Element of tfsm by Def2;

          take qai, qbi;

          thus qai = (((qa,w) -admissible ) . (i + 1)) by A6;

          thus qbi = (((qb,w) -admissible ) . (i + 1)) by A6;

          qai = qa by Def2;

          hence thesis by A1, Def2;

        end;

          suppose

           A7: i in ( Seg ( len w));

          then

           A8: 1 <= i & i <= ( len w) by FINSEQ_1: 1;

          then

          consider wi be Element of IAlph, qai9,qai19 be Element of tfsm such that

           A9: wi = (w . i) & qai9 = (((qa,w) -admissible ) . i) and

           A10: qai19 = (((qa,w) -admissible ) . (i + 1)) and

           A11: (wi -succ_of qai9) = qai19 by Def2;

          take qai19;

          consider wi9 be Element of IAlph, qbi9,qbi19 be Element of tfsm such that

           A12: wi9 = (w . i) & qbi9 = (((qb,w) -admissible ) . i) and

           A13: qbi19 = (((qb,w) -admissible ) . (i + 1)) and

           A14: (wi9 -succ_of qbi9) = qbi19 by A8, Def2;

          take qbi19;

          thus qai19 = (((qa,w) -admissible ) . (i + 1)) by A10;

          thus qbi19 = (((qb,w) -admissible ) . (i + 1)) by A13;

          thus thesis by A3, A7, A9, A11, A12, A14, Th19;

        end;

      end;

      

       A15: ( Seg ( len w)) = ( dom w) by FINSEQ_1:def 3;

      

       A16: P[ 0 ] by FINSEQ_1: 1;

      for i be Nat holds P[i] from NAT_1:sch 2( A16, A2);

      hence thesis by A15;

    end;

    definition

      let IAlph, OAlph, tfsm, qa, qb;

      let k be Nat;

      :: FSM_1:def11

      pred k -equivalent qa,qb means for w st ( len w) <= k holds ((qa,w) -response ) = ((qb,w) -response );

    end

    theorem :: FSM_1:21

    

     Th21: for k be Nat holds k -equivalent (qa,qa);

    theorem :: FSM_1:22

    

     Th22: for k be Nat st k -equivalent (qa,qb) holds k -equivalent (qb,qa);

    theorem :: FSM_1:23

    

     Th23: for k be Nat st k -equivalent (qa,qb) & k -equivalent (qb,qc) holds k -equivalent (qa,qc)

    proof

      let k be Nat;

      assume that

       A1: k -equivalent (qa,qb) and

       A2: k -equivalent (qb,qc);

      thus k -equivalent (qa,qc)

      proof

        let w be FinSequence of IAlph;

        assume

         A3: ( len w) <= k;

        then ((qa,w) -response ) = ((qb,w) -response ) by A1;

        hence thesis by A2, A3;

      end;

    end;

    theorem :: FSM_1:24

    (qa,qb) -are_equivalent implies k -equivalent (qa,qb);

    theorem :: FSM_1:25

    

     Th25: 0 -equivalent (qa,qb)

    proof

      let w be FinSequence of IAlph;

      assume ( len w) <= 0 ;

      then

       A1: w = ( <*> IAlph);

      

      hence ((qa,w) -response ) = ( <*> OAlph) by Th9

      .= ((qb,w) -response ) by A1, Th9;

    end;

    theorem :: FSM_1:26

    

     Th26: for k,m be Nat st (k + m) -equivalent (qa,qb) holds k -equivalent (qa,qb)

    proof

      let k,m be Nat;

      assume

       A1: (k + m) -equivalent (qa,qb);

      let w be FinSequence of IAlph;

      

       A2: k <= (k + m) by NAT_1: 11;

      assume ( len w) <= k;

      then ( len w) <= (k + m) by A2, XXREAL_0: 2;

      hence thesis by A1;

    end;

    theorem :: FSM_1:27

    

     Th27: for k be Nat st 1 <= k holds (k -equivalent (qa,qb) iff 1 -equivalent (qa,qb) & for s be Element of IAlph, k1 be Nat st k1 = (k - 1) holds k1 -equivalent ((the Tran of tfsm . [qa, s]),(the Tran of tfsm . [qb, s])))

    proof

      let k be Nat;

      set OF = the OFun of tfsm;

      assume

       A1: 1 <= k;

      hereby

        assume

         A2: k -equivalent (qa,qb);

        thus

         A3: 1 -equivalent (qa,qb) by A1, XXREAL_0: 2, A2;

        let s be Element of IAlph, k1 be Nat such that

         A4: k1 = (k - 1);

        set qb9 = (the Tran of tfsm . [qb, s]);

        set qa9 = (the Tran of tfsm . [qa, s]);

        thus k1 -equivalent (qa9,qb9)

        proof

          let w be FinSequence of IAlph;

          set sw = ( <*s*> ^ w);

          

           A5: ( len <*s*>) = 1 by FINSEQ_1: 40;

          assume ( len w) <= k1;

          then

           A6: (( len w) + 1) <= (k1 + 1) by XREAL_1: 7;

          ( len ( <*s*> ^ w)) = (( len <*s*>) + ( len w)) by FINSEQ_1: 22

          .= (1 + ( len w)) by FINSEQ_1: 40;

          then

           A7: ((qa,sw) -response ) = ((qb,sw) -response ) by A2, A4, A6;

          

           A8: ((qa,sw) -response ) = ( <*(OF . [qa, s])*> ^ ((qa9,w) -response )) & ((qb,sw) -response ) = ( <*(OF . [qb, s])*> ^ ((qb9,w) -response )) by Th18;

          ( 0 + 1) in ( Seg ( 0 + 1)) by FINSEQ_1: 4;

          then

           A9: 1 in ( dom <*s*>) by A5, FINSEQ_1:def 3;

          (OF . [qa, s]) = (OF . [(((qa, <*s*>) -admissible ) . 1), s]) by Def2

          .= (OF . [(((qa, <*s*>) -admissible ) . 1), ( <*s*> . 1)]) by FINSEQ_1:def 8

          .= (((qa, <*s*>) -response ) . 1) by A9, Def6

          .= (((qb, <*s*>) -response ) . 1) by A3, A5

          .= (OF . [(((qb, <*s*>) -admissible ) . 1), ( <*s*> . 1)]) by A9, Def6

          .= (OF . [(((qb, <*s*>) -admissible ) . 1), s]) by FINSEQ_1:def 8

          .= (OF . [qb, s]) by Def2;

          hence thesis by A8, A7, FINSEQ_1: 33;

        end;

      end;

      assume that

       A10: 1 -equivalent (qa,qb) and

       A11: for s be Element of IAlph, k1 be Nat st k1 = (k - 1) holds k1 -equivalent ((the Tran of tfsm . [qa, s]),(the Tran of tfsm . [qb, s]));

      thus k -equivalent (qa,qb)

      proof

        let w be FinSequence of IAlph such that

         A12: ( len w) <= k;

        per cases ;

          suppose

           A13: w = ( <*> IAlph);

          

          hence ((qa,w) -response ) = ( <*> OAlph) by Th9

          .= ((qb,w) -response ) by A13, Th9;

        end;

          suppose w is non empty;

          then

          consider s be Element of IAlph, w9 be FinSequence of IAlph such that s = (w . 1) and

           A14: w = ( <*s*> ^ w9) by FINSEQ_3: 102;

          reconsider k1 = (k - 1) as Element of NAT by A1, INT_1: 5;

          

           A15: ( len <*s*>) = 1 by FINSEQ_1: 40;

          ( len w) = (( len <*s*>) + ( len w9)) by A14, FINSEQ_1: 22

          .= (( len w9) + 1) by FINSEQ_1: 40;

          then

           A16: ((( len w9) + 1) - 1) <= k1 by A12, XREAL_1: 9;

          ( 0 + 1) in ( Seg ( 0 + 1)) by FINSEQ_1: 4;

          then

           A17: 1 in ( dom <*s*>) by A15, FINSEQ_1:def 3;

          set qa9 = (the Tran of tfsm . [qa, s]), qb9 = (the Tran of tfsm . [qb, s]);

          

           A18: ((qa,w) -response ) = ( <*(OF . [qa, s])*> ^ ((qa9,w9) -response )) & ((qb,w) -response ) = ( <*(OF . [qb, s])*> ^ ((qb9,w9) -response )) by A14, Th18;

          

           A19: k1 -equivalent (qa9,qb9) by A11;

          (OF . [qa, s]) = (OF . [(((qa, <*s*>) -admissible ) . 1), s]) by Def2

          .= (OF . [(((qa, <*s*>) -admissible ) . 1), ( <*s*> . 1)]) by FINSEQ_1:def 8

          .= (((qa, <*s*>) -response ) . 1) by A17, Def6

          .= (((qb, <*s*>) -response ) . 1) by A10, A15

          .= (OF . [(((qb, <*s*>) -admissible ) . 1), ( <*s*> . 1)]) by A17, Def6

          .= (OF . [(((qb, <*s*>) -admissible ) . 1), s]) by FINSEQ_1:def 8

          .= (OF . [qb, s]) by Def2;

          hence thesis by A18, A19, A16;

        end;

      end;

    end;

    definition

      let IAlph, OAlph, tfsm;

      let i be Nat;

      :: FSM_1:def12

      func i -eq_states_EqR tfsm -> Equivalence_Relation of the carrier of tfsm means

      : Def12: for qa, qb holds [qa, qb] in it iff i -equivalent (qa,qb);

      existence

      proof

        set S = the carrier of tfsm;

        defpred P[ object, object] means ex qa,qb be Element of S st qa = $1 & qb = $2 & i -equivalent (qa,qb);

        

         A1: for x,y be object st P[x, y] holds P[y, x] by Th22;

        

         A2: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by Th23;

        

         A3: for x be object st x in S holds P[x, x] by Th21;

        consider EqR be Equivalence_Relation of S such that

         A4: for x,y be object holds [x, y] in EqR iff x in S & y in S & P[x, y] from EQREL_1:sch 1( A3, A1, A2);

        take EqR;

        let qa,qb be Element of S;

        hereby

          assume [qa, qb] in EqR;

          then ex qa9,qb9 be Element of S st qa9 = qa & qb9 = qb & i -equivalent (qa9,qb9) by A4;

          hence i -equivalent (qa,qb);

        end;

        assume i -equivalent (qa,qb);

        hence thesis by A4;

      end;

      uniqueness

      proof

        set S = the carrier of tfsm;

        let IT1,IT2 be Equivalence_Relation of S;

        assume

         A5: for qa,qb be Element of S holds [qa, qb] in IT1 iff i -equivalent (qa,qb);

        assume

         A6: for qa,qb be Element of S holds [qa, qb] in IT2 iff i -equivalent (qa,qb);

        assume IT1 <> IT2;

        then

        consider x be object such that

         A7: x in IT1 & not x in IT2 or x in IT2 & not x in IT1 by TARSKI: 2;

        per cases by A7;

          suppose

           A8: x in IT1 & not x in IT2;

          then

          consider qa,qb be object such that

           A9: x = [qa, qb] and

           A10: qa in S & qb in S by RELSET_1: 2;

          reconsider qa, qb as Element of S by A10;

          i -equivalent (qa,qb) by A5, A8, A9;

          hence contradiction by A6, A8, A9;

        end;

          suppose

           A11: x in IT2 & not x in IT1;

          then

          consider qa,qb be object such that

           A12: x = [qa, qb] and

           A13: qa in S & qb in S by RELSET_1: 2;

          reconsider qa, qb as Element of S by A13;

          i -equivalent (qa,qb) by A6, A11, A12;

          hence contradiction by A5, A11, A12;

        end;

      end;

    end

    definition

      let IAlph, OAlph;

      let tfsm be non empty Mealy-FSM over IAlph, OAlph;

      let i be Nat;

      :: FSM_1:def13

      func i -eq_states_partition tfsm -> non empty a_partition of the carrier of tfsm equals ( Class (i -eq_states_EqR tfsm));

      coherence ;

    end

    theorem :: FSM_1:28

    

     Th28: ((k + 1) -eq_states_partition tfsm) is_finer_than (k -eq_states_partition tfsm)

    proof

      set K = (k -eq_states_partition tfsm);

      set K1 = ((k + 1) -eq_states_partition tfsm);

      set S = the carrier of tfsm;

      let X be set;

      assume

       A1: X in K1;

      then

      reconsider X9 = X as Subset of S;

      consider q be Element of S such that

       A2: q in X by A1, FINSEQ_4: 87;

      reconsider Y = (( proj K) . q) as Element of K;

      take Y;

      thus Y in K;

      let x be object;

      assume

       A3: x in X;

      then x in X9;

      then

      reconsider x9 = x as Element of S;

      reconsider X9 as Element of ( Class ((k + 1) -eq_states_EqR tfsm)) by A1;

      consider Q be object such that Q in S and

       A4: X9 = ( Class (((k + 1) -eq_states_EqR tfsm),Q)) by EQREL_1:def 3;

       [x9, Q] in ((k + 1) -eq_states_EqR tfsm) by A3, A4, EQREL_1: 19;

      then

       A5: [Q, x9] in ((k + 1) -eq_states_EqR tfsm) by EQREL_1: 6;

       [q, Q] in ((k + 1) -eq_states_EqR tfsm) by A2, A4, EQREL_1: 19;

      then [q, x9] in ((k + 1) -eq_states_EqR tfsm) by A5, EQREL_1: 7;

      then (k + 1) -equivalent (q,x9) by Def12;

      then k -equivalent (q,x9) by Th26;

      then [q, x9] in (k -eq_states_EqR tfsm) by Def12;

      then

       A6: [x9, q] in (k -eq_states_EqR tfsm) by EQREL_1: 6;

      reconsider Y9 = Y as Element of ( Class (k -eq_states_EqR tfsm));

      consider Q be object such that

       A7: Q in S and

       A8: Y9 = ( Class ((k -eq_states_EqR tfsm),Q)) by EQREL_1:def 3;

      reconsider Q as Element of S by A7;

      q in Y by EQREL_1:def 9;

      then ( Class ((k -eq_states_EqR tfsm),Q)) = ( Class ((k -eq_states_EqR tfsm),q)) by A8, EQREL_1: 23;

      hence thesis by A6, A8, EQREL_1: 19;

    end;

    theorem :: FSM_1:29

    

     Th29: for k be Nat holds ( Class (k -eq_states_EqR tfsm)) = ( Class ((k + 1) -eq_states_EqR tfsm)) implies for m be Nat holds ( Class ((k + m) -eq_states_EqR tfsm)) = ( Class (k -eq_states_EqR tfsm))

    proof

      let k be Nat;

      set S = the carrier of tfsm;

      set CEk = ( Class (k -eq_states_EqR tfsm));

      set Ek = (k -eq_states_EqR tfsm);

      set CEk1 = ( Class ((k + 1) -eq_states_EqR tfsm));

      set Ek1 = ((k + 1) -eq_states_EqR tfsm);

      defpred P[ Nat] means ( Class ((k + $1) -eq_states_EqR tfsm)) = CEk;

      assume CEk = CEk1;

      then

       A1: Ek = Ek1 by FINSEQ_4: 86;

      

       A2: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        set CEkm = ( Class ((k + m) -eq_states_EqR tfsm));

        set Ekm = ((k + m) -eq_states_EqR tfsm);

        set CEkm1 = ( Class ((k + (m + 1)) -eq_states_EqR tfsm));

        set Ekm1 = ((k + (m + 1)) -eq_states_EqR tfsm);

        assume CEkm = CEk;

        then

         A3: Ekm = Ek by FINSEQ_4: 86;

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          hereby

            assume

             A4: x in CEkm1;

            then

            reconsider x9 = x as Subset of S;

            consider qa be object such that

             A5: qa in S and

             A6: x9 = ( Class (Ekm1,qa)) by A4, EQREL_1:def 3;

            reconsider qa as Element of S by A5;

            

             A7: x9 c= S;

            now

              let y be object;

              hereby

                assume

                 A8: y in xx;

                then

                reconsider y9 = y as Element of S by A7;

                 [y, qa] in Ekm1 by A6, A8, EQREL_1: 19;

                then (k + (m + 1)) -equivalent (y9,qa) by Def12;

                then k -equivalent (y9,qa) by Th26;

                then [y9, qa] in Ek by Def12;

                hence y in ( Class (Ek,qa)) by EQREL_1: 19;

              end;

              assume

               A9: y in ( Class (Ek,qa));

              then

              reconsider y9 = y as Element of S;

               [y9, qa] in Ek by A9, EQREL_1: 19;

              then

               A10: (k + 1) -equivalent (y9,qa) by A1, Def12;

              

               A11: 1 <= (k + 1) by NAT_1: 11;

               A12:

              now

                let s be Element of IAlph, k1 be Nat;

                set Sy9 = (the Tran of tfsm . [y9, s]);

                set Sqa = (the Tran of tfsm . [qa, s]);

                k in NAT & k = ((k + 1) - 1) by ORDINAL1:def 12;

                then k -equivalent (Sy9,Sqa) by A10, A11, Th27;

                then

                 A13: [Sy9, Sqa] in Ek by Def12;

                assume k1 = (((k + m) + 1) - 1);

                hence k1 -equivalent (Sy9,Sqa) by A3, A13, Def12;

              end;

              1 <= ((k + m) + 1) & 1 -equivalent (y9,qa) by A10, A11, Th27, NAT_1: 11;

              then ((k + m) + 1) -equivalent (y9,qa) by A12, Th27;

              then [y9, qa] in Ekm1 by Def12;

              hence y in xx by A6, EQREL_1: 19;

            end;

            then x = ( Class (Ek,qa)) by TARSKI: 2;

            hence x in CEk by EQREL_1:def 3;

          end;

          assume

           A14: x in CEk;

          then

          reconsider x9 = x as Subset of S;

          consider qa be object such that

           A15: qa in S and

           A16: x9 = ( Class (Ek,qa)) by A14, EQREL_1:def 3;

          reconsider qa as Element of S by A15;

          now

            let y be object;

            hereby

              assume

               A17: y in xx;

              then

              reconsider y9 = y as Element of S by A16;

               [y9, qa] in Ek by A16, A17, EQREL_1: 19;

              then

               A18: (k + 1) -equivalent (y9,qa) by A1, Def12;

              

               A19: 1 <= (k + 1) by NAT_1: 11;

               A20:

              now

                let s be Element of IAlph, k1 be Nat;

                set Sy9 = (the Tran of tfsm . [y9, s]);

                set Sqa = (the Tran of tfsm . [qa, s]);

                k in NAT & k = ((k + 1) - 1) by ORDINAL1:def 12;

                then k -equivalent (Sy9,Sqa) by A18, A19, Th27;

                then

                 A21: [Sy9, Sqa] in Ek by Def12;

                assume k1 = (((k + m) + 1) - 1);

                hence k1 -equivalent (Sy9,Sqa) by A3, A21, Def12;

              end;

              1 <= ((k + m) + 1) & 1 -equivalent (y9,qa) by A18, A19, Th27, NAT_1: 11;

              then ((k + m) + 1) -equivalent (y9,qa) by A20, Th27;

              then [y9, qa] in Ekm1 by Def12;

              hence y in ( Class (Ekm1,qa)) by EQREL_1: 19;

            end;

            assume

             A22: y in ( Class (Ekm1,qa));

            then

            reconsider y9 = y as Element of S;

             [y, qa] in Ekm1 by A22, EQREL_1: 19;

            then (k + (m + 1)) -equivalent (y9,qa) by Def12;

            then k -equivalent (y9,qa) by Th26;

            then [y9, qa] in Ek by Def12;

            hence y in xx by A16, EQREL_1: 19;

          end;

          then x = ( Class (Ekm1,qa)) by TARSKI: 2;

          hence x in CEkm1 by EQREL_1:def 3;

        end;

        hence CEkm1 = CEk by TARSKI: 2;

      end;

      

       A23: P[ 0 ];

      thus for m be Nat holds P[m] from NAT_1:sch 2( A23, A2);

    end;

    theorem :: FSM_1:30

    (k -eq_states_partition tfsm) = ((k + 1) -eq_states_partition tfsm) implies for m holds ((k + m) -eq_states_partition tfsm) = (k -eq_states_partition tfsm) by Th29;

    theorem :: FSM_1:31

    

     Th31: ((k + 1) -eq_states_partition tfsm) <> (k -eq_states_partition tfsm) implies for i st i <= k holds ((i + 1) -eq_states_partition tfsm) <> (i -eq_states_partition tfsm)

    proof

      assume

       A1: ((k + 1) -eq_states_partition tfsm) <> (k -eq_states_partition tfsm);

      let i be Nat such that

       A2: i <= k;

      

       A3: ex e be Nat st (k + 1) = (i + e) by A2, NAT_1: 10, NAT_1: 12;

      assume

       A4: ((i + 1) -eq_states_partition tfsm) = (i -eq_states_partition tfsm);

      ex d be Nat st k = (i + d) by A2, NAT_1: 10;

      then (k -eq_states_partition tfsm) = (i -eq_states_partition tfsm) by A4, Th29;

      hence contradiction by A1, A4, A3, Th29;

    end;

    theorem :: FSM_1:32

    

     Th32: for tfsm be finite non empty Mealy-FSM over IAlph, OAlph holds (k -eq_states_partition tfsm) = ((k + 1) -eq_states_partition tfsm) or ( card (k -eq_states_partition tfsm)) < ( card ((k + 1) -eq_states_partition tfsm))

    proof

      let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;

      set kp = (k -eq_states_partition tfsm);

      set k1p = ((k + 1) -eq_states_partition tfsm);

      ( card kp) <= ( card k1p) by Th28, FINSEQ_4: 89;

      then

       A1: ( card kp) = ( card k1p) or ( card kp) < ( card k1p) by XXREAL_0: 1;

      assume kp <> k1p;

      hence thesis by A1, Th28, FINSEQ_4: 91;

    end;

    theorem :: FSM_1:33

    

     Th33: ( Class (( 0 -eq_states_EqR tfsm),q)) = the carrier of tfsm

    proof

      set 0e = ( 0 -eq_states_EqR tfsm);

      set S = the carrier of tfsm;

      now

        let z be object;

        thus z in ( Class (0e,q)) implies z in S;

        assume z in S;

        then

        reconsider z9 = z as Element of S;

         0 -equivalent (z9,q) by Th25;

        then [z, q] in 0e by Def12;

        hence z in ( Class (0e,q)) by EQREL_1: 19;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FSM_1:34

    ( 0 -eq_states_partition tfsm) = {the carrier of tfsm}

    proof

      set S = the carrier of tfsm;

      set SS = {the carrier of tfsm};

      set 0p = ( 0 -eq_states_partition tfsm);

      set 0e = ( 0 -eq_states_EqR tfsm);

      now

        set y = the Element of S;

        let x be object;

        hereby

          assume

           A1: x in 0p;

          then

          reconsider x9 = x as Subset of S;

          consider y be object such that

           A2: y in S and

           A3: x9 = ( Class (0e,y)) by A1, EQREL_1:def 3;

          reconsider y as Element of S by A2;

          ( Class (0e,y)) = S by Th33;

          hence x in SS by A3, TARSKI:def 1;

        end;

        assume x in SS;

        then

         A4: x = S by TARSKI:def 1;

        ( Class (0e,y)) in ( Class 0e) by EQREL_1:def 3;

        hence x in 0p by A4, Th33;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FSM_1:35

    

     Th35: for tfsm be finite non empty Mealy-FSM over IAlph, OAlph st (n + 1) = ( card the carrier of tfsm) holds ((n + 1) -eq_states_partition tfsm) = (n -eq_states_partition tfsm)

    proof

      let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;

      assume

       A1: (n + 1) = ( card the carrier of tfsm);

      defpred P[ Nat] means $1 <= (n + 1) implies ( card ($1 -eq_states_partition tfsm)) > $1;

      assume

       A2: ((n + 1) -eq_states_partition tfsm) <> (n -eq_states_partition tfsm);

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: k <= (n + 1) implies ( card (k -eq_states_partition tfsm)) > k;

        assume

         A5: (k + 1) <= (n + 1);

        then k <= n by XREAL_1: 6;

        then

         A6: ((k + 1) -eq_states_partition tfsm) <> (k -eq_states_partition tfsm) by A2, Th31;

        (k + 1) <= ( card (k -eq_states_partition tfsm)) by A4, A5, NAT_1: 13;

        hence thesis by A6, Th32, XXREAL_0: 2;

      end;

      

       A7: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A7, A3);

      then ( card ((n + 1) -eq_states_partition tfsm)) > (n + 1);

      hence contradiction by A1, FINSEQ_4: 88;

    end;

    definition

      let IAlph, OAlph;

      let tfsm be non empty Mealy-FSM over IAlph, OAlph;

      let IT be a_partition of the carrier of tfsm;

      :: FSM_1:def14

      attr IT is final means for qa,qb be State of tfsm holds (qa,qb) -are_equivalent iff ex X be Element of IT st qa in X & qb in X;

    end

    theorem :: FSM_1:36

    (k -eq_states_partition tfsm) is final implies ((k + 1) -eq_states_EqR tfsm) = (k -eq_states_EqR tfsm)

    proof

      set S = the carrier of tfsm;

      set keq = (k -eq_states_EqR tfsm);

      set k1eq = ((k + 1) -eq_states_EqR tfsm);

      set kpart = (k -eq_states_partition tfsm);

      assume

       A1: (k -eq_states_partition tfsm) is final;

      now

        let x be object;

        hereby

          assume

           A2: x in k1eq;

          then

          consider a,b be object such that

           A3: x = [a, b] and

           A4: a in S and

           A5: b in S by RELSET_1: 2;

          reconsider b as Element of S by A5;

          reconsider a as Element of S by A4;

          (k + 1) -equivalent (a,b) by A2, A3, Def12;

          then k -equivalent (a,b) by Th26;

          hence x in keq by A3, Def12;

        end;

        assume

         A6: x in keq;

        then

        consider a,b be object such that

         A7: x = [a, b] and

         A8: a in S and

         A9: b in S by RELSET_1: 2;

        reconsider b as Element of S by A9;

        reconsider a as Element of S by A8;

        reconsider cl = ( Class (keq,b)) as Element of kpart by EQREL_1:def 3;

        

         A10: b in cl by EQREL_1: 20;

        a in cl by A6, A7, EQREL_1: 19;

        then (a,b) -are_equivalent by A1, A10;

        then (k + 1) -equivalent (a,b);

        hence x in k1eq by A7, Def12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FSM_1:37

    

     Th37: (k -eq_states_partition tfsm) = ((k + 1) -eq_states_partition tfsm) implies (k -eq_states_partition tfsm) is final

    proof

      set S = the carrier of tfsm;

      set kpart = (k -eq_states_partition tfsm);

      set k1part = ((k + 1) -eq_states_partition tfsm);

      set keq = (k -eq_states_EqR tfsm);

      assume

       A1: kpart = k1part;

      now

        let qa,qb be Element of tfsm;

        hereby

          reconsider X = ( Class (keq,qb)) as Element of kpart by EQREL_1:def 3;

          assume

           A2: (qa,qb) -are_equivalent ;

          take X;

          k -equivalent (qa,qb) by A2;

          then [qa, qb] in keq by Def12;

          hence qa in X & qb in X by EQREL_1: 19, EQREL_1: 20;

        end;

        given X be Element of kpart such that

         A3: qa in X and

         A4: qb in X;

        consider qc be object such that qc in S and

         A5: X = ( Class (keq,qc)) by EQREL_1:def 3;

         [qb, qc] in keq by A4, A5, EQREL_1: 19;

        then

         A6: [qc, qb] in keq by EQREL_1: 6;

         [qa, qc] in keq by A3, A5, EQREL_1: 19;

        then

         A7: [qa, qb] in keq by A6, EQREL_1: 7;

        then

         A8: k -equivalent (qa,qb) by Def12;

        thus (qa,qb) -are_equivalent

        proof

          let w be FinSequence of IAlph;

          consider n be Nat such that

           A9: ( dom w) = ( Seg n) by FINSEQ_1:def 2;

          n in NAT by ORDINAL1:def 12;

          then

           A10: n = ( len w) by A9, FINSEQ_1:def 3;

          per cases ;

            suppose n <= k;

            hence thesis by A8, A10;

          end;

            suppose n > k;

            then ex m be Element of NAT st n = (k + m) & 1 <= m by FINSEQ_4: 84;

            then (n -eq_states_partition tfsm) = kpart by A1, Th29;

            then [qa, qb] in (n -eq_states_EqR tfsm) by A7, FINSEQ_4: 86;

            then n -equivalent (qa,qb) by Def12;

            hence thesis by A10;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FSM_1:38

    for tfsm be finite non empty Mealy-FSM over IAlph, OAlph st (n + 1) = ( card the carrier of tfsm) holds ex k be Nat st k <= n & (k -eq_states_partition tfsm) is final

    proof

      let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;

      assume

       A1: (n + 1) = ( card the carrier of tfsm);

      take n;

      thus n <= n;

      (n -eq_states_partition tfsm) = ((n + 1) -eq_states_partition tfsm) by A1, Th35;

      hence thesis by Th37;

    end;

    definition

      let IAlph, OAlph;

      let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;

      :: FSM_1:def15

      func final_states_partition tfsm -> a_partition of the carrier of tfsm means

      : Def15: it is final;

      existence

      proof

        reconsider n = ( card the carrier of tfsm) as Nat;

        consider m be Nat such that

         A1: n = (m + 1) by NAT_1: 6;

        reconsider m as Nat;

        take (m -eq_states_partition tfsm);

        (m -eq_states_partition tfsm) = ((m + 1) -eq_states_partition tfsm) by A1, Th35;

        hence thesis by Th37;

      end;

      uniqueness

      proof

        let it1,it2 be a_partition of the carrier of tfsm;

        assume that

         A2: it1 is final and

         A3: it2 is final;

        now

          assume it1 <> it2;

          then not for X be object holds X in it1 iff X in it2 by TARSKI: 2;

          then

          consider X be set such that

           A4: X in it1 & not X in it2 or not X in it1 & X in it2;

          per cases by A4;

            suppose

             A5: X in it1 & not X in it2;

            then

            reconsider X as Subset of tfsm;

            consider qx be Element of tfsm such that

             A6: qx in X by A5, FINSEQ_4: 87;

            ( union it2) = the carrier of tfsm by EQREL_1:def 4;

            then

            consider Z be set such that

             A7: qx in Z and

             A8: Z in it2 by TARSKI:def 4;

            reconsider Z as Subset of tfsm by A8;

            set XZ = (X \ Z), ZX = (Z \ X), Y9 = (XZ \/ ZX);

            Y9 <> {}

            proof

              assume

               A9: Y9 = {} ;

              then (Z \ X) = {} ;

              then

               A10: Z c= X by XBOOLE_1: 37;

              (X \ Z) = {} by A9;

              then X c= Z by XBOOLE_1: 37;

              hence contradiction by A5, A8, A10, XBOOLE_0:def 10;

            end;

            then

            consider qy be Element of tfsm such that

             A11: qy in Y9 by SUBSET_1: 4;

            reconsider X as Element of it1 by A5;

             A12:

            now

              assume

               A13: qy in (Z \ X);

              

               A14: not (qx,qy) -are_equivalent

              proof

                assume (qx,qy) -are_equivalent ;

                then

                consider Z9 be Element of it1 such that

                 A15: qx in Z9 and

                 A16: qy in Z9 by A2;

                per cases ;

                  suppose X = Z9;

                  hence contradiction by A13, A16, XBOOLE_0:def 5;

                end;

                  suppose X <> Z9;

                  then X misses Z9 by EQREL_1:def 4;

                  then (X /\ Z9) = {} ;

                  hence contradiction by A6, A15, XBOOLE_0:def 4;

                end;

              end;

              qy in Z by A13, XBOOLE_0:def 5;

              hence contradiction by A3, A7, A8, A14;

            end;

            now

              assume

               A17: qy in (X \ Z);

              

               A18: not (qx,qy) -are_equivalent

              proof

                assume (qx,qy) -are_equivalent ;

                then

                consider Z9 be Element of it2 such that

                 A19: qx in Z9 and

                 A20: qy in Z9 by A3;

                per cases ;

                  suppose Z = Z9;

                  hence contradiction by A17, A20, XBOOLE_0:def 5;

                end;

                  suppose Z <> Z9;

                  then Z misses Z9 by A8, EQREL_1:def 4;

                  then (Z /\ Z9) = {} ;

                  hence contradiction by A7, A19, XBOOLE_0:def 4;

                end;

              end;

              qy in X by A17, XBOOLE_0:def 5;

              hence contradiction by A2, A6, A18;

            end;

            hence contradiction by A11, A12, XBOOLE_0:def 3;

          end;

            suppose

             A21: not X in it1 & X in it2;

            then

            reconsider X as Subset of tfsm;

            consider qx be Element of tfsm such that

             A22: qx in X by A21, FINSEQ_4: 87;

            ( union it1) = the carrier of tfsm by EQREL_1:def 4;

            then

            consider Z be set such that

             A23: qx in Z and

             A24: Z in it1 by TARSKI:def 4;

            reconsider Z as Subset of tfsm by A24;

            set XZ = (X \ Z);

            set ZX = (Z \ X);

            set Y9 = (XZ \/ ZX);

            Y9 <> {}

            proof

              assume

               A25: Y9 = {} ;

              then (Z \ X) = {} ;

              then

               A26: Z c= X by XBOOLE_1: 37;

              (X \ Z) = {} by A25;

              then X c= Z by XBOOLE_1: 37;

              hence contradiction by A21, A24, A26, XBOOLE_0:def 10;

            end;

            then

            consider qy be Element of tfsm such that

             A27: qy in Y9 by SUBSET_1: 4;

            reconsider X as Element of it2 by A21;

             A28:

            now

              assume

               A29: qy in (Z \ X);

              

               A30: not (qx,qy) -are_equivalent

              proof

                assume (qx,qy) -are_equivalent ;

                then

                consider Z9 be Element of it2 such that

                 A31: qx in Z9 and

                 A32: qy in Z9 by A3;

                per cases ;

                  suppose X = Z9;

                  hence contradiction by A29, A32, XBOOLE_0:def 5;

                end;

                  suppose X <> Z9;

                  then X misses Z9 by EQREL_1:def 4;

                  then (X /\ Z9) = {} ;

                  hence contradiction by A22, A31, XBOOLE_0:def 4;

                end;

              end;

              qy in Z by A29, XBOOLE_0:def 5;

              hence contradiction by A2, A23, A24, A30;

            end;

            now

              assume

               A33: qy in (X \ Z);

              

               A34: not (qx,qy) -are_equivalent

              proof

                assume (qx,qy) -are_equivalent ;

                then

                consider Z9 be Element of it1 such that

                 A35: qx in Z9 and

                 A36: qy in Z9 by A2;

                per cases ;

                  suppose Z = Z9;

                  hence contradiction by A33, A36, XBOOLE_0:def 5;

                end;

                  suppose Z <> Z9;

                  then Z misses Z9 by A24, EQREL_1:def 4;

                  then (Z /\ Z9) = {} ;

                  hence contradiction by A23, A35, XBOOLE_0:def 4;

                end;

              end;

              qy in X by A33, XBOOLE_0:def 5;

              hence contradiction by A3, A22, A34;

            end;

            hence contradiction by A27, A28, XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: FSM_1:39

    

     Th39: for tfsm be finite non empty Mealy-FSM over IAlph, OAlph holds (n + 1) = ( card the carrier of tfsm) implies ( final_states_partition tfsm) = (n -eq_states_partition tfsm)

    proof

      let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;

      assume (n + 1) = ( card the carrier of tfsm);

      then ((n + 1) -eq_states_partition tfsm) = (n -eq_states_partition tfsm) by Th35;

      then (n -eq_states_partition tfsm) is final by Th37;

      hence thesis by Def15;

    end;

    begin

    reserve tfsm,rtfsm for finite non empty Mealy-FSM over IAlph, OAlph,

q for State of tfsm;

    definition

      let IAlph,OAlph be non empty set;

      let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;

      let qf be Element of ( final_states_partition tfsm);

      let s be Element of IAlph;

      :: FSM_1:def16

      func (s,qf) -succ_class -> Element of ( final_states_partition tfsm) means

      : Def16: ex q be State of tfsm, n be Nat st q in qf & (n + 1) = ( card the carrier of tfsm) & it = ( Class ((n -eq_states_EqR tfsm),(the Tran of tfsm . [q, s])));

      existence

      proof

        consider q1 be Element of tfsm such that

         A1: q1 in qf by FINSEQ_4: 87;

        set q9 = (the Tran of tfsm . [q1, s]);

        set m = ( card the carrier of tfsm);

        consider n be Nat such that

         A2: m = (n + 1) by NAT_1: 6;

        reconsider n as Nat;

        ( final_states_partition tfsm) = (n -eq_states_partition tfsm) by A2, Th39;

        then

        reconsider IT = ( Class ((n -eq_states_EqR tfsm),q9)) as Element of ( final_states_partition tfsm) by EQREL_1:def 3;

        take IT;

        thus thesis by A2, A1;

      end;

      uniqueness

      proof

        let it1,it2 be Element of ( final_states_partition tfsm);

        given q1 be Element of tfsm, n1 be Nat such that

         A3: q1 in qf and

         A4: (n1 + 1) = ( card the carrier of tfsm) & it1 = ( Class ((n1 -eq_states_EqR tfsm),(the Tran of tfsm . [q1, s])));

        set q19 = (the Tran of tfsm . [q1, s]);

        given q2 be Element of tfsm, n2 be Nat such that

         A5: q2 in qf and

         A6: (n2 + 1) = ( card the carrier of tfsm) & it2 = ( Class ((n2 -eq_states_EqR tfsm),(the Tran of tfsm . [q2, s])));

        set q29 = (the Tran of tfsm . [q2, s]), m = (n1 + 1);

        

         A7: 1 <= m & n1 = (m - 1) by NAT_1: 11;

        ( final_states_partition tfsm) is final by Def15;

        then (q1,q2) -are_equivalent by A3, A5;

        then m -equivalent (q1,q2);

        then n1 -equivalent (q19,q29) by A7, Th27;

        then [q19, q29] in (n1 -eq_states_EqR tfsm) by Def12;

        hence thesis by A4, A6, EQREL_1: 35;

      end;

    end

    definition

      let IAlph, OAlph, tfsm;

      let qf be Element of ( final_states_partition tfsm), s;

      :: FSM_1:def17

      func (qf,s) -class_response -> Element of OAlph means

      : Def17: ex q st q in qf & it = (the OFun of tfsm . [q, s]);

      existence

      proof

        consider q1 be Element of tfsm such that

         A1: q1 in qf by FINSEQ_4: 87;

        take (the OFun of tfsm . [q1, s]);

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Element of OAlph;

        given q1 be Element of tfsm such that

         A2: q1 in qf and

         A3: it1 = (the OFun of tfsm . [q1, s]);

        given q2 be Element of tfsm such that

         A4: q2 in qf and

         A5: it2 = (the OFun of tfsm . [q2, s]);

        ( final_states_partition tfsm) is final by Def15;

        then (q1,q2) -are_equivalent by A2, A4;

        hence thesis by A3, A5, Th19;

      end;

    end

    definition

      let IAlph, OAlph, tfsm;

      :: FSM_1:def18

      func the_reduction_of tfsm -> strict Mealy-FSM over IAlph, OAlph means

      : Def18: the carrier of it = ( final_states_partition tfsm) & (for Q be State of it , s holds for q be State of tfsm st q in Q holds (the Tran of tfsm . (q,s)) in (the Tran of it . (Q,s)) & (the OFun of tfsm . (q,s)) = (the OFun of it . (Q,s))) & the InitS of tfsm in the InitS of it ;

      existence

      proof

        set part = ( final_states_partition tfsm);

        reconsider m = ( card the carrier of tfsm) as Nat;

        set TR = the Tran of tfsm;

        consider n be Nat such that

         A1: m = (n + 1) by NAT_1: 6;

        reconsider n as Nat;

        set IS = ( Class ((n -eq_states_EqR tfsm),the InitS of tfsm));

        part = (n -eq_states_partition tfsm) by A1, Th39;

        then

        reconsider IS as Element of part by EQREL_1:def 3;

        deffunc F( Element of part, Element of IAlph) = (($2,$1) -succ_class );

        consider Trf be Function of [:part, IAlph:], part such that

         A2: for q be Element of part holds for i be Element of IAlph holds (Trf . (q,i)) = F(q,i) from BINOP_1:sch 4;

        deffunc F( Element of part, Element of IAlph) = (($1,$2) -class_response );

        consider OF be Function of [:part, IAlph:], OAlph such that

         A3: for q be Element of part holds for i be Element of IAlph holds (OF . (q,i)) = F(q,i) from BINOP_1:sch 4;

        take IT = Mealy-FSM (# ( final_states_partition tfsm), Trf, OF, IS #);

        now

          reconsider a19 = 1 as Integer;

          let Q be Element of IT, s, q such that

           A4: q in Q;

          reconsider s9 = s as Element of IAlph;

          reconsider Q9 = Q as Element of ( final_states_partition tfsm);

          consider Q1 be Element of tfsm, n1 be Nat such that

           A5: Q1 in Q9 and (n1 + 1) = ( card the carrier of tfsm) and

           A6: ((s9,Q9) -succ_class ) = ( Class ((n1 -eq_states_EqR tfsm),(TR . [Q1, s9]))) by Def16;

          ( final_states_partition tfsm) is final by Def15;

          then (q,Q1) -are_equivalent by A4, A5;

          then

           A7: (n1 + 1) -equivalent (q,Q1);

          reconsider n19 = n1 as Integer;

          1 <= (n1 + 1) & ((n19 + a19) - a19) = n19 by NAT_1: 11;

          then n1 -equivalent ((TR . [q, s9]),(TR . [Q1, s9])) by A7, Th27;

          then

           A8: [(TR . [q, s9]), (TR . [Q1, s9])] in (n1 -eq_states_EqR tfsm) by Def12;

          (the Tran of IT . (Q9,s9)) = ( Class ((n1 -eq_states_EqR tfsm),(TR . (Q1,s9)))) by A2, A6;

          hence (TR . [q, s]) in (the Tran of IT . (Q,s)) by A8, EQREL_1: 19;

          

           A9: (the OFun of IT . (Q9,s9)) = ((Q9,s9) -class_response ) by A3;

          consider Q1 be Element of tfsm such that

           A10: Q1 in Q9 and

           A11: ((Q9,s9) -class_response ) = (the OFun of tfsm . [Q1, s9]) by Def17;

          ( final_states_partition tfsm) is final by Def15;

          then (q,Q1) -are_equivalent by A4, A10;

          hence (the OFun of tfsm . [q, s]) = (the OFun of IT . [Q, s]) by A9, A11, Th19;

        end;

        hence thesis by EQREL_1: 20;

      end;

      uniqueness

      proof

        let it1,it2 be strict Mealy-FSM over IAlph, OAlph;

        set TR = the Tran of tfsm;

        assume that

         A12: the carrier of it1 = ( final_states_partition tfsm) and

         A13: for Q be Element of it1, s, q st q in Q holds (TR . (q,s)) in (the Tran of it1 . (Q,s)) & (the OFun of tfsm . (q,s)) = (the OFun of it1 . (Q,s)) and

         A14: the InitS of tfsm in the InitS of it1;

        assume that

         A15: the carrier of it2 = ( final_states_partition tfsm) and

         A16: for Q be Element of it2, s, q st q in Q holds (TR . (q,s)) in (the Tran of it2 . (Q,s)) & (the OFun of tfsm . (q,s)) = (the OFun of it2 . (Q,s)) and

         A17: the InitS of tfsm in the InitS of it2;

        

         A18: the OFun of it1 = the OFun of it2

        proof

          reconsider OF2 = the OFun of it2 as Function of [:( final_states_partition tfsm), IAlph:], OAlph by A15;

          reconsider OF1 = the OFun of it1 as Function of [:( final_states_partition tfsm), IAlph:], OAlph by A12;

          now

            let Q be Element of ( final_states_partition tfsm), s;

            consider q be Element of tfsm such that

             A19: q in Q by FINSEQ_4: 87;

            

            thus (OF1 . (Q,s)) = (the OFun of tfsm . (q,s)) by A12, A13, A19

            .= (OF2 . (Q,s)) by A15, A16, A19;

          end;

          hence thesis by BINOP_1: 2;

        end;

        

         A20: the Tran of it1 = the Tran of it2

        proof

          reconsider T2 = the Tran of it2 as Function of [:( final_states_partition tfsm), IAlph:], ( final_states_partition tfsm) by A15;

          reconsider T1 = the Tran of it1 as Function of [:( final_states_partition tfsm), IAlph:], ( final_states_partition tfsm) by A12;

          now

            let Q be Element of ( final_states_partition tfsm), s;

            reconsider T19 = (T1 . [Q, s]), T29 = (T2 . [Q, s]) as Subset of tfsm by TARSKI:def 3;

            

             A21: T19 = T29 or T19 misses T29 by EQREL_1:def 4;

            consider q be Element of tfsm such that

             A22: q in Q by FINSEQ_4: 87;

            (TR . (q,s)) in (T1 . (Q,s)) & (TR . (q,s)) in (T2 . (Q,s)) by A12, A13, A15, A16, A22;

            hence (T1 . (Q,s)) = (T2 . (Q,s)) by A21, XBOOLE_0: 3;

          end;

          hence thesis by BINOP_1: 2;

        end;

        the InitS of it1 = the InitS of it2

        proof

          the InitS of it2 in ( final_states_partition tfsm) by A15;

          then

          reconsider IS2 = the InitS of it2 as Subset of tfsm;

          the InitS of it1 in ( final_states_partition tfsm) by A12;

          then

          reconsider IS1 = the InitS of it1 as Subset of tfsm;

          IS1 = IS2 or IS1 misses IS2 by A12, A15, EQREL_1:def 4;

          hence thesis by A14, A17, XBOOLE_0: 3;

        end;

        hence thesis by A12, A15, A20, A18;

      end;

    end

    registration

      let IAlph, OAlph, tfsm;

      cluster ( the_reduction_of tfsm) -> non empty finite;

      coherence

      proof

        the carrier of ( the_reduction_of tfsm) = ( final_states_partition tfsm) by Def18;

        hence thesis;

      end;

    end

    theorem :: FSM_1:40

    

     Th40: for qr be State of rtfsm st rtfsm = ( the_reduction_of tfsm) & q in qr holds for k be Nat st k in ( Seg (( len w) + 1)) holds (((q,w) -admissible ) . k) in (((qr,w) -admissible ) . k)

    proof

      let qr be State of rtfsm;

      set TR = the Tran of tfsm;

      assume that

       A1: rtfsm = ( the_reduction_of tfsm) and

       A2: q in qr;

      defpred P[ Nat] means $1 in ( Seg (( len w) + 1)) implies (((q,w) -admissible ) . $1) in (((qr,w) -admissible ) . $1);

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: k in ( Seg (( len w) + 1)) implies (((q,w) -admissible ) . k) in (((qr,w) -admissible ) . k);

        assume

         A5: (k + 1) in ( Seg (( len w) + 1));

        

         A6: k = 0 or 0 < k & ( 0 + 1) = 1;

        per cases by A6, NAT_1: 13;

          suppose

           A7: k = 0 ;

          then (((q,w) -admissible ) . (k + 1)) = q by Def2;

          hence thesis by A2, A7, Def2;

        end;

          suppose

           A8: 1 <= k;

          

           A9: (k + 1) <= (( len w) + 1) by A5, FINSEQ_1: 1;

          then

           A10: k <= ( len w) by XREAL_1: 6;

          then

          consider w1i be Element of IAlph, q1i,q1i1 be Element of tfsm such that

           A11: w1i = (w . k) & q1i = (((q,w) -admissible ) . k) and

           A12: q1i1 = (((q,w) -admissible ) . (k + 1)) & (w1i -succ_of q1i) = q1i1 by A8, Def2;

          consider w2i be Element of IAlph, q2i,q2i1 be Element of rtfsm such that

           A13: w2i = (w . k) & q2i = (((qr,w) -admissible ) . k) and

           A14: q2i1 = (((qr,w) -admissible ) . (k + 1)) & (w2i -succ_of q2i) = q2i1 by A8, A10, Def2;

          k <= (k + 1) by NAT_1: 11;

          then k <= (( len w) + 1) by A9, XXREAL_0: 2;

          then (TR . (q1i,w1i)) in (the Tran of rtfsm . (q2i,w2i)) by A1, A4, A8, A11, A13, Def18, FINSEQ_1: 1;

          hence thesis by A12, A14;

        end;

      end;

      

       A15: P[ 0 ] by FINSEQ_1: 1;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A15, A3);

    end;

    theorem :: FSM_1:41

    

     Th41: (tfsm,( the_reduction_of tfsm)) -are_equivalent

    proof

      now

        set rtfsm = ( the_reduction_of tfsm);

        let w1 be FinSequence of IAlph;

        set ad1 = ((the InitS of tfsm,w1) -admissible );

        set ad2 = ((the InitS of rtfsm,w1) -admissible );

        set r1 = ((the InitS of tfsm,w1) -response );

        set r2 = ((the InitS of rtfsm,w1) -response );

        

         A1: the InitS of tfsm in the InitS of rtfsm by Def18;

         A2:

        now

          let k be Nat;

          assume that

           A3: 1 <= k and

           A4: k <= ( len r1);

          k <= ( len w1) by A4, Def6;

          then

           A5: k in ( Seg ( len w1)) by A3, FINSEQ_1: 1;

          then

           A6: k in ( Seg (( len w1) + 1)) by FINSEQ_2: 8;

          then

           A7: (ad1 . k) in (ad2 . k) by A1, Th40;

          k in ( Seg ( len ad2)) by A6, Def2;

          then k in ( dom ad2) by FINSEQ_1:def 3;

          then

           A8: (ad2 . k) is Element of rtfsm by FINSEQ_2: 11;

          k in ( Seg ( len ad1)) by A6, Def2;

          then k in ( dom ad1) by FINSEQ_1:def 3;

          then

           A9: (ad1 . k) is Element of tfsm by FINSEQ_2: 11;

          

           A10: k in ( dom w1) by A5, FINSEQ_1:def 3;

          then

           A11: (w1 . k) is Element of IAlph by FINSEQ_2: 11;

          

          thus (r2 . k) = (the OFun of rtfsm . ((ad2 . k),(w1 . k))) by A10, Def6

          .= (the OFun of tfsm . ((ad1 . k),(w1 . k))) by A9, A11, A8, A7, Def18

          .= (r1 . k) by A10, Def6;

        end;

        ( len r1) = ( len w1) by Def6

        .= ( len r2) by Def6;

        hence r1 = r2 by A2, FINSEQ_1: 14;

      end;

      hence thesis;

    end;

    begin

    reserve qr1,qr2 for State of rtfsm,

Tf for Function of the carrier of tfsm1, the carrier of tfsm2;

    definition

      let IAlph, OAlph, tfsm1, tfsm2;

      :: FSM_1:def19

      pred tfsm1,tfsm2 -are_isomorphic means ex Tf st Tf is bijective & (Tf . the InitS of tfsm1) = the InitS of tfsm2 & for q11, s holds (Tf . (the Tran of tfsm1 . (q11,s))) = (the Tran of tfsm2 . ((Tf . q11),s)) & (the OFun of tfsm1 . (q11,s)) = (the OFun of tfsm2 . ((Tf . q11),s));

      reflexivity

      proof

        let tfsm1 be non empty Mealy-FSM over IAlph, OAlph;

        take Tf = ( id the carrier of tfsm1);

        thus Tf is bijective;

        thus (Tf . the InitS of tfsm1) = the InitS of tfsm1;

        let q be Element of tfsm1, s;

        

        thus (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm1 . [q, s])

        .= (the Tran of tfsm1 . ((Tf . q),s));

        thus thesis;

      end;

      symmetry

      proof

        let tfsm1,tfsm2 be non empty Mealy-FSM over IAlph, OAlph;

        given Tf be Function of the carrier of tfsm1, the carrier of tfsm2 such that

         A1: Tf is bijective and

         A2: (Tf . the InitS of tfsm1) = the InitS of tfsm2 and

         A3: for q be Element of tfsm1, s be Element of IAlph holds (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm2 . ((Tf . q),s)) & (the OFun of tfsm1 . (q,s)) = (the OFun of tfsm2 . ((Tf . q),s));

        

         A4: ( dom Tf) = the carrier of tfsm1 by FUNCT_2:def 1;

        then

         A5: ( rng (Tf " )) = the carrier of tfsm1 by A1, FUNCT_1: 33;

        

         A6: ( rng Tf) = the carrier of tfsm2 by A1, FUNCT_2:def 3;

        then the carrier of tfsm2 = ( dom (Tf " )) by A1, FUNCT_1: 33;

        then

        reconsider Tf9 = (Tf " ) as Function of the carrier of tfsm2, the carrier of tfsm1 by A5, FUNCT_2: 1;

        take Tf9;

        Tf9 is onto by A5, FUNCT_2:def 3;

        hence Tf9 is bijective by A1;

        thus the InitS of tfsm1 = (Tf9 . the InitS of tfsm2) by A1, A2, A4, FUNCT_1: 34;

        now

          let q be Element of tfsm2, s be Element of IAlph;

          

           A7: q = (Tf . (Tf9 . q)) by A1, A6, FUNCT_1: 35;

          

          thus (the Tran of tfsm1 . [(Tf9 . q), s]) = (Tf9 . (Tf . (the Tran of tfsm1 . ((Tf9 . q),s)))) by A1, A4, FUNCT_1: 34

          .= (Tf9 . (the Tran of tfsm2 . (q,s))) by A3, A7;

          thus (the OFun of tfsm1 . ((Tf9 . q),s)) = (the OFun of tfsm2 . (q,s)) by A3, A7;

        end;

        hence thesis;

      end;

    end

    theorem :: FSM_1:42

    

     Th42: (tfsm1,tfsm2) -are_isomorphic & (tfsm2,tfsm3) -are_isomorphic implies (tfsm1,tfsm3) -are_isomorphic

    proof

      assume that

       A1: (tfsm1,tfsm2) -are_isomorphic and

       A2: (tfsm2,tfsm3) -are_isomorphic ;

      consider Tf1 be Function of the carrier of tfsm1, the carrier of tfsm2 such that

       A3: Tf1 is bijective and

       A4: (Tf1 . the InitS of tfsm1) = the InitS of tfsm2 and

       A5: for q be Element of tfsm1, s1 be Element of IAlph holds (Tf1 . (the Tran of tfsm1 . (q,s1))) = (the Tran of tfsm2 . ((Tf1 . q),s1)) & (the OFun of tfsm1 . (q,s1)) = (the OFun of tfsm2 . ((Tf1 . q),s1)) by A1;

      consider Tf2 be Function of the carrier of tfsm2, the carrier of tfsm3 such that

       A6: Tf2 is bijective and

       A7: (Tf2 . the InitS of tfsm2) = the InitS of tfsm3 and

       A8: for q be Element of tfsm2, s1 be Element of IAlph holds (Tf2 . (the Tran of tfsm2 . (q,s1))) = (the Tran of tfsm3 . ((Tf2 . q),s1)) & (the OFun of tfsm2 . (q,s1)) = (the OFun of tfsm3 . ((Tf2 . q),s1)) by A2;

      take Tf = (Tf2 * Tf1);

      thus Tf is bijective by A3, A6, FINSEQ_4: 85;

      

       A9: ( dom Tf1) = the carrier of tfsm1 by FUNCT_2:def 1;

      hence (Tf . the InitS of tfsm1) = the InitS of tfsm3 by A4, A7, FUNCT_1: 13;

      now

        let q be Element of tfsm1, s1 be Element of IAlph;

        

        thus (the Tran of tfsm3 . [(Tf . q), s1]) = (the Tran of tfsm3 . ((Tf2 . (Tf1 . q)),s1)) by A9, FUNCT_1: 13

        .= (Tf2 . (the Tran of tfsm2 . ((Tf1 . q),s1))) by A8

        .= (Tf2 . (Tf1 . (the Tran of tfsm1 . (q,s1)))) by A5

        .= (Tf . (the Tran of tfsm1 . (q,s1))) by A9, FUNCT_1: 13;

        

        thus (the OFun of tfsm3 . [(Tf . q), s1]) = (the OFun of tfsm3 . ((Tf2 . (Tf1 . q)),s1)) by A9, FUNCT_1: 13

        .= (the OFun of tfsm2 . ((Tf1 . q),s1)) by A8

        .= (the OFun of tfsm1 . (q,s1)) by A5;

      end;

      hence thesis;

    end;

    theorem :: FSM_1:43

    

     Th43: (for q be State of tfsm1, s holds (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm2 . ((Tf . q),s))) implies for k st 1 <= k & k <= (( len w) + 1) holds (Tf . (((q11,w) -admissible ) . k)) = ((((Tf . q11),w) -admissible ) . k)

    proof

      defpred P[ Nat] means 1 <= $1 & $1 <= (( len w) + 1) implies (Tf . (((q11,w) -admissible ) . $1)) = ((((Tf . q11),w) -admissible ) . $1);

      assume

       A1: for q be State of tfsm1, s holds (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm2 . ((Tf . q),s));

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: 1 <= k & k <= (( len w) + 1) implies (Tf . (((q11,w) -admissible ) . k)) = ((((Tf . q11),w) -admissible ) . k);

        assume that 1 <= (k + 1) and

         A4: (k + 1) <= (( len w) + 1);

        

         A5: k = 0 or 0 < k & ( 0 + 1) = 1;

        per cases by A5, NAT_1: 13;

          suppose

           A6: k = 0 ;

          

          hence (Tf . (((q11,w) -admissible ) . (k + 1))) = (Tf . q11) by Def2

          .= ((((Tf . q11),w) -admissible ) . (k + 1)) by A6, Def2;

        end;

          suppose

           A7: 1 <= k;

          

           A8: ( len w) <= (( len w) + 1) by NAT_1: 11;

          

           A9: k <= ( len w) by A4, XREAL_1: 6;

          then

          consider wi be Element of IAlph, qi,qi1 be State of tfsm1 such that

           A10: wi = (w . k) & qi = (((q11,w) -admissible ) . k) and

           A11: qi1 = (((q11,w) -admissible ) . (k + 1)) & (wi -succ_of qi) = qi1 by A7, Def2;

          consider wri be Element of IAlph, qri,qri1 be State of tfsm2 such that

           A12: wri = (w . k) & qri = ((((Tf . q11),w) -admissible ) . k) and

           A13: qri1 = ((((Tf . q11),w) -admissible ) . (k + 1)) & (wri -succ_of qri) = qri1 by A7, A9, Def2;

          

          thus (Tf . (((q11,w) -admissible ) . (k + 1))) = (Tf . (the Tran of tfsm1 . (qi,wi))) by A11

          .= (the Tran of tfsm2 . (qri,wri)) by A1, A3, A7, A9, A8, A10, A12, XXREAL_0: 2

          .= ((((Tf . q11),w) -admissible ) . (k + 1)) by A13;

        end;

      end;

      

       A14: P[ 0 ];

      thus for k be Nat holds P[k] from NAT_1:sch 2( A14, A2);

    end;

    theorem :: FSM_1:44

    

     Th44: (for q be State of tfsm1, s holds (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm2 . ((Tf . q),s)) & (the OFun of tfsm1 . (q,s)) = (the OFun of tfsm2 . ((Tf . q),s))) implies ((q11,q12) -are_equivalent iff ((Tf . q11),(Tf . q12)) -are_equivalent )

    proof

      set Stfsm1 = the carrier of tfsm1;

      set Stfsm2 = the carrier of tfsm2;

      set OF1 = the OFun of tfsm1, OF2 = the OFun of tfsm2;

      assume

       A1: for q be Element of Stfsm1, s holds (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm2 . ((Tf . q),s)) & (the OFun of tfsm1 . (q,s)) = (the OFun of tfsm2 . ((Tf . q),s));

      hereby

        reconsider Tq2 = (Tf . q12) as Element of Stfsm2;

        reconsider Tq1 = (Tf . q11) as Element of Stfsm2;

        assume

         A2: (q11,q12) -are_equivalent ;

        now

          let w be FinSequence of IAlph;

           A3:

          now

            let k be Nat;

            assume that

             A4: 1 <= k and

             A5: k <= ( len ((Tq1,w) -response ));

            ( len ((Tq1,w) -response )) = ( len w) by Def6;

            then

             A6: k in ( Seg ( len w)) by A4, A5, FINSEQ_1: 1;

            then

             A7: k in ( Seg (( len w) + 1)) by FINSEQ_2: 8;

            then

             A8: k <= (( len w) + 1) by FINSEQ_1: 1;

            ( len ((q11,w) -admissible )) = (( len w) + 1) by Def2;

            then k in ( dom ((q11,w) -admissible )) by A7, FINSEQ_1:def 3;

            then

            reconsider q1a = (((q11,w) -admissible ) . k) as Element of Stfsm1 by FINSEQ_2: 11;

            ( len ((q12,w) -admissible )) = (( len w) + 1) by Def2;

            then k in ( dom ((q12,w) -admissible )) by A7, FINSEQ_1:def 3;

            then

            reconsider q2a = (((q12,w) -admissible ) . k) as Element of Stfsm1 by FINSEQ_2: 11;

            

             A9: k in ( dom w) by A6, FINSEQ_1:def 3;

            then

            reconsider wk = (w . k) as Element of IAlph by FINSEQ_2: 11;

            

            thus (((Tq1,w) -response ) . k) = (OF2 . [(((Tq1,w) -admissible ) . k), (w . k)]) by A9, Def6

            .= (OF2 . ((Tf . q1a),wk)) by A1, A4, A8, Th43

            .= (OF1 . (q1a,wk)) by A1

            .= (((q11,w) -response ) . k) by A9, Def6

            .= (((q12,w) -response ) . k) by A2

            .= (OF1 . (q2a,wk)) by A9, Def6

            .= (OF2 . ((Tf . q2a),wk)) by A1

            .= (OF2 . [(((Tq2,w) -admissible ) . k), (w . k)]) by A1, A4, A8, Th43

            .= (((Tq2,w) -response ) . k) by A9, Def6;

          end;

          ( len ((Tq1,w) -response )) = ( len w) by Def6

          .= ( len ((Tq2,w) -response )) by Def6;

          hence ((Tq1,w) -response ) = ((Tq2,w) -response ) by A3, FINSEQ_1: 14;

        end;

        hence ((Tf . q11),(Tf . q12)) -are_equivalent ;

      end;

      assume

       A10: ((Tf . q11),(Tf . q12)) -are_equivalent ;

      now

        let w be FinSequence of IAlph;

         A11:

        now

          let k be Nat;

          assume that

           A12: 1 <= k and

           A13: k <= ( len ((q11,w) -response ));

          ( len ((q11,w) -response )) = ( len w) by Def6;

          then

           A14: k in ( Seg ( len w)) by A12, A13, FINSEQ_1: 1;

          then

           A15: k in ( Seg (( len w) + 1)) by FINSEQ_2: 8;

          then

           A16: k in NAT & k <= (( len w) + 1) by FINSEQ_1: 1;

          ( len ((q12,w) -admissible )) = (( len w) + 1) by Def2;

          then k in ( dom ((q12,w) -admissible )) by A15, FINSEQ_1:def 3;

          then

          reconsider q2a = (((q12,w) -admissible ) . k) as Element of Stfsm1 by FINSEQ_2: 11;

          ( len ((q11,w) -admissible )) = (( len w) + 1) by Def2;

          then k in ( dom ((q11,w) -admissible )) by A15, FINSEQ_1:def 3;

          then

          reconsider q1a = (((q11,w) -admissible ) . k) as Element of Stfsm1 by FINSEQ_2: 11;

          

           A17: k in ( dom w) by A14, FINSEQ_1:def 3;

          then

          reconsider wk = (w . k) as Element of IAlph by FINSEQ_2: 11;

          

          thus (((q11,w) -response ) . k) = (OF1 . ((((q11,w) -admissible ) . k),(w . k))) by A17, Def6

          .= (OF2 . ((Tf . q1a),wk)) by A1

          .= (OF2 . [((((Tf . q11),w) -admissible ) . k), wk]) by A1, A12, A16, Th43

          .= ((((Tf . q11),w) -response ) . k) by A17, Def6

          .= ((((Tf . q12),w) -response ) . k) by A10

          .= (OF2 . [((((Tf . q12),w) -admissible ) . k), (w . k)]) by A17, Def6

          .= (OF2 . ((Tf . q2a),wk)) by A1, A12, A16, Th43

          .= (OF1 . (q2a,(w . k))) by A1

          .= (((q12,w) -response ) . k) by A17, Def6;

        end;

        ( len ((q11,w) -response )) = ( len w) by Def6

        .= ( len ((q12,w) -response )) by Def6;

        hence ((q11,w) -response ) = ((q12,w) -response ) by A11, FINSEQ_1: 14;

      end;

      hence thesis;

    end;

    theorem :: FSM_1:45

    

     Th45: rtfsm = ( the_reduction_of tfsm) & qr1 <> qr2 implies not (qr1,qr2) -are_equivalent

    proof

      assume that

       A1: rtfsm = ( the_reduction_of tfsm) and

       A2: qr1 <> qr2;

      

       A3: the carrier of rtfsm = ( final_states_partition tfsm) by A1, Def18;

      then

      reconsider q19 = qr1 as Subset of tfsm by TARSKI:def 3;

      consider x be Element of tfsm such that

       A4: x in q19 by A3, FINSEQ_4: 87;

      reconsider q29 = qr2 as Subset of tfsm by A3, TARSKI:def 3;

      consider y be Element of tfsm such that

       A5: y in q29 by A3, FINSEQ_4: 87;

      

       A6: ( final_states_partition tfsm) is final by Def15;

       not (x,y) -are_equivalent

      proof

        assume (x,y) -are_equivalent ;

        then

        consider X be Element of rtfsm such that

         A7: x in X & y in X by A3, A6;

        

         A8: q29 misses q19 by A2, A3, EQREL_1:def 4;

        X is Subset of tfsm by A3, TARSKI:def 3;

        then X = q19 or X misses q19 by A3, EQREL_1:def 4;

        hence contradiction by A4, A5, A7, A8, XBOOLE_0: 3;

      end;

      then

      consider w be FinSequence of IAlph such that

       A9: ((x,w) -response ) <> ((y,w) -response );

      set q1adm = ((qr1,w) -admissible ), q2adm = ((qr2,w) -admissible );

      set xadm = ((x,w) -admissible ), yadm = ((y,w) -admissible );

      set xresp = ((x,w) -response ), yresp = ((y,w) -response );

      ( len xresp) = ( len w) by Def6

      .= ( len yresp) by Def6;

      then

      consider k be Nat such that

       A10: 1 <= k & k <= ( len xresp) and

       A11: (xresp . k) <> (yresp . k) by A9, FINSEQ_1: 14;

      ( len xresp) = ( len w) by Def6;

      then

       A12: k in ( Seg ( len w)) by A10, FINSEQ_1: 1;

      then k in ( Seg (( len w) + 1)) by FINSEQ_2: 8;

      then

       A13: (yadm . k) in (q2adm . k) by A1, A5, Th40;

      set q1resp = ((qr1,w) -response ), q2resp = ((qr2,w) -response );

      

       A14: ( len q1adm) = (( len w) + 1) by Def2

      .= (( len xresp) + 1) by Def6;

      k in ( Seg ( len xresp)) by A10, FINSEQ_1: 1;

      then

       A15: k in ( Seg ( len q1adm)) by A14, FINSEQ_2: 8;

      then k in ( dom q1adm) by FINSEQ_1:def 3;

      then

       A16: (q1adm . k) is Element of rtfsm by FINSEQ_2: 11;

      ( len q2adm) = (( len w) + 1) by Def2

      .= ( len q1adm) by Def2;

      then k in ( dom q2adm) by A15, FINSEQ_1:def 3;

      then

       A17: (q2adm . k) is Element of rtfsm by FINSEQ_2: 11;

      k in ( dom w) by A12, FINSEQ_1:def 3;

      then

       A18: (w . k) is Element of IAlph by FINSEQ_2: 11;

      

       A19: ( len q1adm) = (( len w) + 1) by Def2

      .= ( len xadm) by Def2;

      then k in ( dom xadm) by A15, FINSEQ_1:def 3;

      then

       A20: (xadm . k) is Element of tfsm by FINSEQ_2: 11;

      ( len yadm) = (( len w) + 1) by Def2

      .= ( len xadm) by Def2;

      then k in ( dom yadm) by A15, A19, FINSEQ_1:def 3;

      then

       A21: (yadm . k) is Element of tfsm by FINSEQ_2: 11;

      k in ( Seg (( len w) + 1)) by A12, FINSEQ_2: 8;

      then

       A22: (xadm . k) in (q1adm . k) by A1, A4, Th40;

      now

        assume

         A23: q1resp = q2resp;

        ( len w) = ( len xresp) by Def6;

        then

         A24: k in ( dom w) by A10, FINSEQ_3: 25;

        then

         A25: (xresp . k) = (the OFun of tfsm . ((xadm . k),(w . k))) by Def6;

        

         A26: (q2resp . k) = (the OFun of rtfsm . ((q2adm . k),(w . k))) by A24, Def6

        .= (the OFun of tfsm . ((yadm . k),(w . k))) by A1, A18, A17, A13, A21, Def18;

        (q1resp . k) = (the OFun of rtfsm . ((q1adm . k),(w . k))) by A24, Def6

        .= (the OFun of tfsm . ((xadm . k),(w . k))) by A1, A16, A18, A22, A20, Def18;

        hence contradiction by A11, A23, A24, A26, A25, Def6;

      end;

      hence thesis;

    end;

    begin

    definition

      let IAlph,OAlph be non empty set;

      let IT be non empty Mealy-FSM over IAlph, OAlph;

      :: FSM_1:def20

      attr IT is reduced means

      : Def20: for qa,qb be State of IT st qa <> qb holds not (qa,qb) -are_equivalent ;

    end

    registration

      let IAlph, OAlph, tfsm;

      cluster ( the_reduction_of tfsm) -> reduced;

      coherence by Th45;

    end

    registration

      let IAlph, OAlph;

      cluster reduced finite for non empty Mealy-FSM over IAlph, OAlph;

      existence

      proof

        set M = the finite non empty Mealy-FSM over IAlph, OAlph;

        take ( the_reduction_of M);

        thus thesis;

      end;

    end

    reserve Rtfsm for reduced finite non empty Mealy-FSM over IAlph, OAlph;

    theorem :: FSM_1:46

    

     Th46: (Rtfsm,( the_reduction_of Rtfsm)) -are_isomorphic

    proof

      set m = Rtfsm;

      set rm = ( the_reduction_of m);

      set fpm = ( final_states_partition m);

      deffunc F( Element of m) = (( proj fpm) . $1);

      consider Tf be Function of the carrier of m, fpm such that

       A1: for q be Element of m holds (Tf . q) = F(q) from FUNCT_2:sch 4;

       A2:

      now

        assume not Tf is one-to-one;

        then

        consider q1,q2 be object such that

         A3: q1 in the carrier of m & q2 in the carrier of m and

         A4: (Tf . q1) = (Tf . q2) and

         A5: q1 <> q2 by FUNCT_2: 19;

        reconsider q1, q2 as State of m by A3;

        (Tf . q1) = (( proj fpm) . q1) by A1;

        then

         A6: q1 in (Tf . q1) by EQREL_1:def 9;

        

         A7: fpm is final by Def15;

        (Tf . q2) = (( proj fpm) . q2) by A1;

        then

         A8: q2 in (Tf . q2) by EQREL_1:def 9;

         not (q1,q2) -are_equivalent by A5, Def20;

        hence contradiction by A4, A7, A6, A8;

      end;

      set Im1 = the InitS of m;

      

       A9: fpm c= ( rng Tf)

      proof

        let x be object;

        assume

         A10: x in fpm;

        then

        reconsider pq = x as Subset of m;

        consider q be Element of m such that

         A11: q in pq by A10, FINSEQ_4: 87;

        pq = (( proj fpm) . q) by A10, A11, EQREL_1: 65;

        then (Tf . q) = pq by A1;

        hence thesis by FUNCT_2: 4;

      end;

      ( rng Tf) c= fpm by RELAT_1:def 19;

      then ( rng Tf) = fpm by A9;

      then

       A12: Tf is onto by FUNCT_2:def 3;

      

       A13: the carrier of rm = fpm by Def18;

       A14:

      now

        let q be State of m, s be Element of IAlph;

        reconsider Tfq = (Tf . q) as State of rm by Def18;

        

         A15: (the Tran of rm . [Tfq, s]) is State of rm;

        (Tf . q) = (( proj fpm) . q) by A1;

        then

         A16: q in (Tf . q) by EQREL_1:def 9;

        then (the Tran of m . (q,s)) in (the Tran of rm . ((Tf . q),s)) by A13, Def18;

        then (the Tran of rm . [(Tf . q), s]) = (( proj fpm) . (the Tran of m . [q, s])) by A13, A15, EQREL_1: 65;

        hence (Tf . (the Tran of m . (q,s))) = (the Tran of rm . ((Tf . q),s)) by A1;

        thus (the OFun of m . (q,s)) = (the OFun of rm . ((Tf . q),s)) by A13, A16, Def18;

      end;

      the InitS of m in the InitS of rm by Def18;

      then the InitS of rm = (( proj fpm) . Im1) by A13, EQREL_1: 65;

      then (Tf . the InitS of m) = the InitS of rm by A1;

      hence thesis by A13, A2, A12, A14;

    end;

    theorem :: FSM_1:47

    

     Th47: tfsm is reduced iff ex M be finite non empty Mealy-FSM over IAlph, OAlph st (tfsm,( the_reduction_of M)) -are_isomorphic

    proof

      set M = tfsm;

      hereby

        assume M is reduced;

        then (M,( the_reduction_of M)) -are_isomorphic by Th46;

        hence ex M be finite non empty Mealy-FSM over IAlph, OAlph st (tfsm,( the_reduction_of M)) -are_isomorphic ;

      end;

      given MM be finite non empty Mealy-FSM over IAlph, OAlph such that

       A1: (M,( the_reduction_of MM)) -are_isomorphic ;

      set rMM = ( the_reduction_of MM);

      consider Tf be Function of the carrier of M, the carrier of rMM such that

       A2: Tf is bijective and (Tf . the InitS of M) = the InitS of rMM and

       A3: for q be State of M, s be Element of IAlph holds (Tf . (the Tran of M . (q,s))) = (the Tran of rMM . ((Tf . q),s)) & (the OFun of M . (q,s)) = (the OFun of rMM . ((Tf . q),s)) by A1;

      let qa,qb be State of M;

      assume qa <> qb;

      then (Tf . qa) <> (Tf . qb) by A2, FUNCT_2: 19;

      then not ((Tf . qa),(Tf . qb)) -are_equivalent by Th45;

      hence thesis by A3, Th44;

    end;

    definition

      let IAlph, OAlph;

      let tfsm be non empty Mealy-FSM over IAlph, OAlph;

      let IT be State of tfsm;

      :: FSM_1:def21

      attr IT is accessible means ex w st (the InitS of tfsm,w) -leads_to IT;

    end

    definition

      let IAlph, OAlph;

      let IT be non empty Mealy-FSM over IAlph, OAlph;

      :: FSM_1:def22

      attr IT is connected means

      : Def22: for q be State of IT holds q is accessible;

    end

    registration

      let IAlph, OAlph;

      cluster connected for finite non empty Mealy-FSM over IAlph, OAlph;

      existence

      proof

        set out = the Element of OAlph;

        reconsider S = {1} as finite non empty set;

        reconsider IS = 1 as Element of S by TARSKI:def 1;

        set dF = [:S, IAlph:];

        set Tr = (dF --> IS);

        reconsider T = Tr as Function of dF, S;

        reconsider OF = (dF --> out) as Function of [:S, IAlph:], OAlph;

        reconsider M = Mealy-FSM (# S, T, OF, IS #) as finite non empty Mealy-FSM over IAlph, OAlph;

        take M;

        let q be State of M;

        q = 1 & (the InitS of M,( <*> IAlph)) -leads_to the InitS of M by Th2, TARSKI:def 1;

        hence thesis;

      end;

    end

    reserve Ctfsm,Ctfsm1,Ctfsm2 for connected finite non empty Mealy-FSM over IAlph, OAlph;

    registration

      let IAlph, OAlph, Ctfsm;

      cluster ( the_reduction_of Ctfsm) -> connected;

      coherence

      proof

        set c = Ctfsm;

        set rtfsm = ( the_reduction_of c);

        

         A1: the InitS of c in the InitS of rtfsm by Def18;

        assume not rtfsm is connected;

        then

        consider Q be State of rtfsm such that

         A2: not Q is accessible;

        

         A3: the carrier of rtfsm = ( final_states_partition c) by Def18;

        then

        reconsider Q9 = Q as Subset of c by TARSKI:def 3;

        Q in the carrier of rtfsm;

        then Q9 in ( final_states_partition c) by Def18;

        then

        consider q be Element of c such that

         A4: q in Q by FINSEQ_4: 87;

        q is accessible by Def22;

        then

        consider w such that

         A5: (the InitS of c,w) -leads_to q;

        1 <= (( len w) + 1) by NAT_1: 11;

        then

         A6: (( len w) + 1) in ( Seg (( len w) + 1)) by FINSEQ_1: 1;

        then (( len w) + 1) in ( Seg ( len ((the InitS of rtfsm,w) -admissible ))) by Def2;

        then (( len w) + 1) in ( dom ((the InitS of rtfsm,w) -admissible )) by FINSEQ_1:def 3;

        then

         A7: (((the InitS of rtfsm,w) -admissible ) . (( len w) + 1)) in the carrier of rtfsm by FINSEQ_2: 11;

        then

        reconsider QQ = (((the InitS of rtfsm,w) -admissible ) . (( len w) + 1)) as Subset of c by A3;

        

         A8: Q9 = QQ or Q9 misses QQ by A3, A7, EQREL_1:def 4;

        (((the InitS of c,w) -admissible ) . (( len w) + 1)) = q by A5;

        then q in (((the InitS of rtfsm,w) -admissible ) . (( len w) + 1)) by A1, A6, Th40;

        then (the InitS of rtfsm,w) -leads_to Q by A4, A8, XBOOLE_0: 3;

        hence contradiction by A2;

      end;

    end

    registration

      let IAlph, OAlph;

      cluster connected reduced finite for non empty Mealy-FSM over IAlph, OAlph;

      existence

      proof

        set cm = the connected finite non empty Mealy-FSM over IAlph, OAlph;

        take ( the_reduction_of cm);

        thus thesis;

      end;

    end

    definition

      let IAlph, OAlph;

      let tfsm be non empty Mealy-FSM over IAlph, OAlph;

      :: FSM_1:def23

      func accessibleStates tfsm -> set equals { q where q be State of tfsm : q is accessible };

      coherence ;

    end

    registration

      let IAlph, OAlph, tfsm;

      cluster ( accessibleStates tfsm) -> finite non empty;

      coherence

      proof

        set m = tfsm;

        set AS = { q where q be State of m : q is accessible };

        

         A1: AS c= the carrier of m

        proof

          let x be object;

          assume x in AS;

          then ex q be State of m st x = q & q is accessible;

          hence thesis;

        end;

        (the InitS of m,( <*> IAlph)) -leads_to the InitS of m by Th2;

        then the InitS of m is accessible;

        then the InitS of m in AS;

        hence thesis by A1;

      end;

    end

    theorem :: FSM_1:48

    

     Th48: ( accessibleStates tfsm) c= the carrier of tfsm & for q holds q in ( accessibleStates tfsm) iff q is accessible

    proof

      set AS = { q where q be State of tfsm : q is accessible };

      AS c= the carrier of tfsm

      proof

        let x be object;

        assume x in AS;

        then ex q be State of tfsm st x = q & q is accessible;

        hence thesis;

      end;

      hence ( accessibleStates tfsm) c= the carrier of tfsm;

      let q be State of tfsm;

      hereby

        assume q in ( accessibleStates tfsm);

        then ex q9 be State of tfsm st q9 = q & q9 is accessible;

        hence q is accessible;

      end;

      thus thesis;

    end;

    theorem :: FSM_1:49

    

     Th49: (the Tran of tfsm | [:( accessibleStates tfsm), IAlph:]) is Function of [:( accessibleStates tfsm), IAlph:], ( accessibleStates tfsm)

    proof

      set cTran = (the Tran of tfsm | [:( accessibleStates tfsm), IAlph:]);

      

       A1: ( accessibleStates tfsm) c= the carrier of tfsm by Th48;

      then [:( accessibleStates tfsm), IAlph:] c= [:the carrier of tfsm, IAlph:] by ZFMISC_1: 96;

      then cTran is Function of [:( accessibleStates tfsm), IAlph:], the carrier of tfsm by FUNCT_2: 32;

      then

       A2: ( dom cTran) = [:( accessibleStates tfsm), IAlph:] by FUNCT_2:def 1;

      ( rng cTran) c= ( accessibleStates tfsm)

      proof

        set I = the InitS of tfsm;

        let x be object;

        assume

         A3: x in ( rng cTran);

        then

        consider d be object such that

         A4: d in ( dom cTran) and

         A5: x = (cTran . d) by FUNCT_1:def 3;

        

         A6: (d `1 ) in ( accessibleStates tfsm) by A2, A4, MCART_1: 10;

        then

        reconsider q = (d `1 ) as State of tfsm by A1;

        reconsider s = (d `2 ) as Element of IAlph by A2, A4, MCART_1: 10;

        set qsa = ((q, <*s*>) -admissible );

        

         A7: (qsa . 1) = q & ( <*s*> . 1) = s by Def2, FINSEQ_1: 40;

        ( rng cTran) c= the carrier of tfsm by RELAT_1:def 19;

        then

        reconsider q1 = x as State of tfsm by A3;

        1 <= ( len <*s*>) by FINSEQ_1: 39;

        then

         A8: ex wi be Element of IAlph, qi,qi1 be State of tfsm st wi = ( <*s*> . 1) & qi = (qsa . 1) & qi1 = (qsa . (1 + 1)) & (wi -succ_of qi) = qi1 by Def2;

        (the Tran of tfsm . d) = q1 by A2, A4, A5, FUNCT_1: 49;

        then

         A9: (qsa . (1 + 1)) = q1 by A4, A7, A8, MCART_1: 21;

        (1 + 1) = 2;

        then

         A10: 2 <= (( len <*s*>) + 1) by FINSEQ_1: 39;

        q is accessible by A6, Th48;

        then

        consider w be FinSequence of IAlph such that

         A11: (I,w) -leads_to q;

        ( len (w ^ <*s*>)) = (( len w) + ( len <*s*>)) by FINSEQ_1: 22;

        

        then (( len (w ^ <*s*>)) + 1) = ((( len w) + 1) + 1) by FINSEQ_1: 39

        .= (( len w) + (1 + 1));

        then (((I,(w ^ <*s*>)) -admissible ) . (( len (w ^ <*s*>)) + 1)) = q1 by A11, A9, A10, Th7;

        then (I,(w ^ <*s*>)) -leads_to q1;

        then q1 is accessible;

        hence thesis;

      end;

      hence thesis by A2, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: FSM_1:50

    for cTran be Function of [:( accessibleStates tfsm), IAlph:], ( accessibleStates tfsm), cOFun be Function of [:( accessibleStates tfsm), IAlph:], OAlph, cInitS be Element of ( accessibleStates tfsm) st cTran = (the Tran of tfsm | [:( accessibleStates tfsm), IAlph:]) & cOFun = (the OFun of tfsm | [:( accessibleStates tfsm), IAlph:]) & cInitS = the InitS of tfsm holds (tfsm, Mealy-FSM (# ( accessibleStates tfsm), cTran, cOFun, cInitS #)) -are_equivalent

    proof

      set M = tfsm;

      let cTran be Function of [:( accessibleStates M), IAlph:], ( accessibleStates M), cOFun be Function of [:( accessibleStates M), IAlph:], OAlph, cInitS be Element of ( accessibleStates M) such that

       A1: cTran = (the Tran of M | [:( accessibleStates M), IAlph:]) and

       A2: cOFun = (the OFun of M | [:( accessibleStates M), IAlph:]) and

       A3: cInitS = the InitS of M;

      let w be FinSequence of IAlph;

      set cm = Mealy-FSM (# ( accessibleStates M), cTran, cOFun, cInitS #);

      set ma = ((the InitS of M,w) -admissible );

      set cma = ((the InitS of cm,w) -admissible );

      set mr = ((the InitS of M,w) -response );

      set cmr = ((the InitS of cm,w) -response );

       A4:

      now

        defpred P[ Nat] means $1 in ( dom ma) implies (ma . $1) = (cma . $1);

        thus ( len ma) = (( len w) + 1) & ( len cma) = (( len w) + 1) by Def2;

        then

         A5: ( dom ma) = ( Seg (( len w) + 1)) by FINSEQ_1:def 3;

        

         A6: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let j be Nat such that

           A7: j in ( dom ma) implies (ma . j) = (cma . j);

          

           A8: 0 = j or 0 < j & ( 0 + 1) = 1;

          assume (j + 1) in ( dom ma);

          then

           A9: (j + 1) <= (( len w) + 1) by A5, FINSEQ_1: 1;

          then

           A10: j <= ( len w) by XREAL_1: 6;

          

           A11: j < (( len w) + 1) by A9, NAT_1: 13;

          per cases by A8, NAT_1: 13;

            suppose

             A12: 0 = j;

            

            hence (ma . (j + 1)) = the InitS of M by Def2

            .= (cma . (j + 1)) by A3, A12, Def2;

          end;

            suppose

             A13: 1 <= j;

            then (ex mwj be Element of IAlph, mqj,mqj1 be State of M st mwj = (w . j) & mqj = (ma . j) & mqj1 = (ma . (j + 1)) & (mwj -succ_of mqj) = mqj1) & ex cmwj be Element of IAlph, cmqj,cmqj1 be State of cm st cmwj = (w . j) & cmqj = (cma . j) & cmqj1 = (cma . (j + 1)) & (cmwj -succ_of cmqj) = cmqj1 by A10, Def2;

            hence thesis by A1, A5, A7, A11, A13, FINSEQ_1: 1, FUNCT_1: 49;

          end;

        end;

        

         A14: P[ 0 ] by A5, FINSEQ_1: 1;

        thus for j be Nat holds P[j] from NAT_1:sch 2( A14, A6);

      end;

      then

       A15: ma = cma by FINSEQ_2: 9;

      now

        thus ( len mr) = ( len w) & ( len cmr) = ( len w) by Def6;

        then

         A16: ( dom mr) = ( Seg ( len w)) by FINSEQ_1:def 3;

        let j be Nat;

        assume

         A17: j in ( dom mr);

        then

         A18: j in ( dom w) by A16, FINSEQ_1:def 3;

        j in ( Seg (( len w) + 1)) by A16, A17, FINSEQ_2: 8;

        then j in ( dom cma) by A4, FINSEQ_1:def 3;

        then

         A19: (cma . j) in ( accessibleStates M) by FINSEQ_2: 11;

        (w . j) in IAlph by A18, FINSEQ_2: 11;

        then

         A20: [(cma . j), (w . j)] in [:( accessibleStates M), IAlph:] by A19, ZFMISC_1: 87;

        

        thus (mr . j) = (the OFun of M . [(ma . j), (w . j)]) by A18, Def6

        .= (cOFun . [(cma . j), (w . j)]) by A2, A15, A20, FUNCT_1: 49

        .= (cmr . j) by A18, Def6;

      end;

      hence thesis by FINSEQ_2: 9;

    end;

    theorem :: FSM_1:51

    ex Ctfsm st the Tran of Ctfsm = (the Tran of tfsm | [:( accessibleStates tfsm), IAlph:]) & the OFun of Ctfsm = (the OFun of tfsm | [:( accessibleStates tfsm), IAlph:]) & the InitS of Ctfsm = the InitS of tfsm & (tfsm,Ctfsm) -are_equivalent

    proof

      set M = tfsm;

      set I = the InitS of M;

      ( accessibleStates M) c= the carrier of M by Th48;

      then [:( accessibleStates M), IAlph:] c= [:the carrier of M, IAlph:] by ZFMISC_1: 96;

      then

      reconsider cOFun = (the OFun of M | [:( accessibleStates M), IAlph:]) as Function of [:( accessibleStates M), IAlph:], OAlph by FUNCT_2: 32;

      (I,( <*> IAlph)) -leads_to I by Th2;

      then I is accessible;

      then

      reconsider cInitS = the InitS of M as Element of ( accessibleStates M) by Th48;

      reconsider cTran = (the Tran of M | [:( accessibleStates M), IAlph:]) as Function of [:( accessibleStates M), IAlph:], ( accessibleStates M) by Th49;

      set cm = Mealy-FSM (# ( accessibleStates M), cTran, cOFun, cInitS #);

       A1:

      now

        let w be FinSequence of IAlph;

        set ma = ((the InitS of M,w) -admissible );

        set cma = ((the InitS of cm,w) -admissible );

        now

          defpred P[ Nat] means $1 in ( dom ma) implies (ma . $1) = (cma . $1);

          thus ( len ma) = (( len w) + 1) & ( len cma) = (( len w) + 1) by Def2;

          then

           A2: ( dom ma) = ( Seg (( len w) + 1)) by FINSEQ_1:def 3;

          

           A3: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let j be Nat such that

             A4: j in ( dom ma) implies (ma . j) = (cma . j);

            

             A5: 0 = j or 0 < j & ( 0 + 1) = 1;

            assume (j + 1) in ( dom ma);

            then

             A6: (j + 1) <= (( len w) + 1) by A2, FINSEQ_1: 1;

            then

             A7: j <= ( len w) by XREAL_1: 6;

            

             A8: j < (( len w) + 1) by A6, NAT_1: 13;

            per cases by A5, NAT_1: 13;

              suppose

               A9: 0 = j;

              

              hence (ma . (j + 1)) = the InitS of M by Def2

              .= (cma . (j + 1)) by A9, Def2;

            end;

              suppose

               A10: 1 <= j;

              then (ex mwj be Element of IAlph, mqj,mqj1 be State of M st mwj = (w . j) & mqj = (ma . j) & mqj1 = (ma . (j + 1)) & (mwj -succ_of mqj) = mqj1) & ex cmwj be Element of IAlph, cmqj,cmqj1 be State of cm st cmwj = (w . j) & cmqj = (cma . j) & cmqj1 = (cma . (j + 1)) & (cmwj -succ_of cmqj) = cmqj1 by A7, Def2;

              hence thesis by A2, A4, A8, A10, FINSEQ_1: 1, FUNCT_1: 49;

            end;

          end;

          

           A11: P[ 0 ] by A2, FINSEQ_1: 1;

          thus for j be Nat holds P[j] from NAT_1:sch 2( A11, A3);

        end;

        hence ma = cma by FINSEQ_2: 9;

      end;

      now

        let q be State of cm;

        q in ( accessibleStates M) & ( accessibleStates M) c= the carrier of M by Th48;

        then

        reconsider q9 = q as State of M;

        q9 is accessible by Th48;

        then

        consider w be FinSequence of IAlph such that

         A12: (the InitS of M,w) -leads_to q9;

        (((the InitS of M,w) -admissible ) . (( len w) + 1)) = q9 by A12;

        then (((the InitS of cm,w) -admissible ) . (( len w) + 1)) = q by A1;

        then (the InitS of cm,w) -leads_to q;

        hence q is accessible;

      end;

      then

      reconsider cm as connected finite non empty Mealy-FSM over IAlph, OAlph by Def22;

      take cm;

      thus the Tran of cm = (the Tran of M | [:( accessibleStates M), IAlph:]);

      thus the OFun of cm = (the OFun of M | [:( accessibleStates M), IAlph:]);

      thus the InitS of cm = the InitS of M;

      let w be FinSequence of IAlph;

      set ma = ((the InitS of M,w) -admissible );

      set cma = ((the InitS of cm,w) -admissible );

      set mr = ((the InitS of M,w) -response );

      set cmr = ((the InitS of cm,w) -response );

      

       A13: ( len cma) = (( len w) + 1) by Def2;

      now

        thus ( len mr) = ( len w) & ( len cmr) = ( len w) by Def6;

        then

         A14: ( dom mr) = ( Seg ( len w)) by FINSEQ_1:def 3;

        let j be Nat;

        assume

         A15: j in ( dom mr);

        then

         A16: j in ( dom w) by A14, FINSEQ_1:def 3;

        j in ( Seg (( len w) + 1)) by A14, A15, FINSEQ_2: 8;

        then j in ( dom cma) by A13, FINSEQ_1:def 3;

        then

         A17: (cma . j) in ( accessibleStates M) by FINSEQ_2: 11;

        (w . j) in IAlph by A16, FINSEQ_2: 11;

        then

         A18: [(cma . j), (w . j)] in [:( accessibleStates M), IAlph:] by A17, ZFMISC_1: 87;

        

         A19: [(ma . j), (w . j)] = [(cma . j), (w . j)] by A1;

        

        thus (mr . j) = (the OFun of M . [(ma . j), (w . j)]) by A16, Def6

        .= (cOFun . [(cma . j), (w . j)]) by A19, A18, FUNCT_1: 49

        .= (cmr . j) by A16, Def6;

      end;

      hence thesis by FINSEQ_2: 9;

    end;

    begin

    definition

      let IAlph be set, OAlph be non empty set;

      let tfsm1,tfsm2 be non empty Mealy-FSM over IAlph, OAlph;

      :: FSM_1:def24

      func tfsm1 -Mealy_union tfsm2 -> strict Mealy-FSM over IAlph, OAlph means

      : Def24: the carrier of it = (the carrier of tfsm1 \/ the carrier of tfsm2) & the Tran of it = (the Tran of tfsm1 +* the Tran of tfsm2) & the OFun of it = (the OFun of tfsm1 +* the OFun of tfsm2) & the InitS of it = the InitS of tfsm1;

      existence

      proof

        set Oftfsm1 = the OFun of tfsm1, Oftfsm2 = the OFun of tfsm2;

        set Trtfsm1 = the Tran of tfsm1, Trtfsm2 = the Tran of tfsm2;

        set Stfsm1 = the carrier of tfsm1, Stfsm2 = the carrier of tfsm2;

        set Tr = (Trtfsm1 +* Trtfsm2), Of = (Oftfsm1 +* Oftfsm2);

        reconsider S = (Stfsm1 \/ Stfsm2) as non empty set;

        ( rng Trtfsm1) c= Stfsm1 & ( rng Trtfsm2) c= Stfsm2 by RELAT_1:def 19;

        then

         A1: ( rng Tr) c= (( rng Trtfsm1) \/ ( rng Trtfsm2)) & (( rng Trtfsm1) \/ ( rng Trtfsm2)) c= (Stfsm1 \/ Stfsm2) by FUNCT_4: 17, XBOOLE_1: 13;

        ( dom Oftfsm1) = [:Stfsm1, IAlph:] & ( dom Oftfsm2) = [:Stfsm2, IAlph:] by FUNCT_2:def 1;

        

        then

         A2: ( dom Of) = ( [:Stfsm1, IAlph:] \/ [:Stfsm2, IAlph:]) by FUNCT_4:def 1

        .= [:(Stfsm1 \/ Stfsm2), IAlph:] by ZFMISC_1: 97;

        ( rng Oftfsm1) c= OAlph & ( rng Oftfsm2) c= OAlph by RELAT_1:def 19;

        then ( rng Of) c= (( rng Oftfsm1) \/ ( rng Oftfsm2)) & (( rng Oftfsm1) \/ ( rng Oftfsm2)) c= (OAlph \/ OAlph) by FUNCT_4: 17, XBOOLE_1: 13;

        then

        reconsider Of as Function of [:S, IAlph:], OAlph by A2, FUNCT_2: 2, XBOOLE_1: 1;

        ( dom Trtfsm1) = [:Stfsm1, IAlph:] & ( dom Trtfsm2) = [:Stfsm2, IAlph:] by FUNCT_2:def 1;

        

        then ( dom Tr) = ( [:Stfsm1, IAlph:] \/ [:Stfsm2, IAlph:]) by FUNCT_4:def 1

        .= [:(Stfsm1 \/ Stfsm2), IAlph:] by ZFMISC_1: 97;

        then

        reconsider Tr as Function of [:S, IAlph:], S by A1, FUNCT_2: 2, XBOOLE_1: 1;

        reconsider IS = the InitS of tfsm1 as Element of S by XBOOLE_0:def 3;

        take Mealy-FSM (# S, Tr, Of, IS #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let IAlph be set, OAlph be non empty set;

      let tfsm1,tfsm2 be non empty finite Mealy-FSM over IAlph, OAlph;

      cluster (tfsm1 -Mealy_union tfsm2) -> non empty finite;

      coherence

      proof

        the carrier of (tfsm1 -Mealy_union tfsm2) = (the carrier of tfsm1 \/ the carrier of tfsm2) by Def24;

        hence thesis;

      end;

    end

    theorem :: FSM_1:52

    

     Th52: tfsm = (tfsm1 -Mealy_union tfsm2) & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q implies ((q11,w) -admissible ) = ((q,w) -admissible )

    proof

      assume that

       A1: tfsm = (tfsm1 -Mealy_union tfsm2) and

       A2: the carrier of tfsm1 misses the carrier of tfsm2 and

       A3: q11 = q;

      set ad1 = ((q11,w) -admissible ), ad = ((q,w) -admissible );

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len ad1) implies (ad1 . $1) = (ad . $1);

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A5: 1 <= k & k <= ( len ad1) implies (ad1 . k) = (ad . k);

        assume that 1 <= (k + 1) and

         A6: (k + 1) <= ( len ad1);

        

         A7: k = 0 or 0 < k & ( 0 + 1) = 1;

        per cases by A7, NAT_1: 13;

          suppose

           A8: k = 0 ;

          

          hence (ad1 . (k + 1)) = q11 by Def2

          .= (ad . (k + 1)) by A3, A8, Def2;

        end;

          suppose

           A9: 1 <= k;

          (k + 1) <= (( len w) + 1) by A6, Def2;

          then

           A10: k <= ( len w) by XREAL_1: 6;

          then

          consider w1k be Element of IAlph, q1k,q1k1 be Element of tfsm1 such that

           A11: w1k = (w . k) & q1k = (ad1 . k) and

           A12: q1k1 = (ad1 . (k + 1)) & (w1k -succ_of q1k) = q1k1 by A9, Def2;

          

           A13: ex wk be Element of IAlph, qk,qk1 be Element of tfsm st wk = (w . k) & qk = (ad . k) & qk1 = (ad . (k + 1)) & (wk -succ_of qk) = qk1 by A9, A10, Def2;

          ( len w) <= (( len w) + 1) by NAT_1: 11;

          then

           A14: k <= (( len w) + 1) by A10, XXREAL_0: 2;

           [:the carrier of tfsm1, IAlph:] misses [:the carrier of tfsm2, IAlph:] by A2, ZFMISC_1: 104;

          then ( dom the Tran of tfsm2) = [:the carrier of tfsm2, IAlph:] & not [q1k, w1k] in [:the carrier of tfsm2, IAlph:] by FUNCT_2:def 1, XBOOLE_0: 3;

          

          hence (ad1 . (k + 1)) = ((the Tran of tfsm1 +* the Tran of tfsm2) . [q1k, w1k]) by A12, FUNCT_4: 11

          .= (ad . (k + 1)) by A1, A5, A9, A11, A13, A14, Def2, Def24;

        end;

      end;

      

       A15: P[ 0 ];

      

       A16: for k be Nat holds P[k] from NAT_1:sch 2( A15, A4);

      ( len ad1) = (( len w) + 1) by Def2

      .= ( len ad) by Def2;

      hence thesis by A16, FINSEQ_1: 14;

    end;

    theorem :: FSM_1:53

    

     Th53: tfsm = (tfsm1 -Mealy_union tfsm2) & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q implies ((q11,w) -response ) = ((q,w) -response )

    proof

      set q1 = q11;

      assume that

       A1: tfsm = (tfsm1 -Mealy_union tfsm2) and

       A2: the carrier of tfsm1 misses the carrier of tfsm2 and

       A3: q1 = q;

      set ad1 = ((q1,w) -admissible );

      set res = ((q,w) -response ), res1 = ((q1,w) -response );

      

       A4: ( len res1) = ( len w) by Def6;

       A5:

      now

        let k be Nat;

        

         A6: [:the carrier of tfsm1, IAlph:] misses [:the carrier of tfsm2, IAlph:] by A2, ZFMISC_1: 104;

        assume 1 <= k & k <= ( len res1);

        then

         A7: k in ( Seg ( len w)) by A4, FINSEQ_1: 1;

        then

         A8: k in ( dom w) by FINSEQ_1:def 3;

        k in ( Seg (( len w) + 1)) by A7, FINSEQ_2: 8;

        then k in ( Seg ( len ad1)) by Def2;

        then k in ( dom ad1) by FINSEQ_1:def 3;

        then

         A9: (ad1 . k) in the carrier of tfsm1 by FINSEQ_2: 11;

        (w . k) in IAlph by A8, FINSEQ_2: 11;

        then [(ad1 . k), (w . k)] in [:the carrier of tfsm1, IAlph:] by A9, ZFMISC_1: 87;

        then

         A10: ( dom the OFun of tfsm2) = [:the carrier of tfsm2, IAlph:] & not [(ad1 . k), (w . k)] in [:the carrier of tfsm2, IAlph:] by A6, FUNCT_2:def 1, XBOOLE_0: 3;

        (res1 . k) = (the OFun of tfsm1 . [(((q1,w) -admissible ) . k), (w . k)]) by A8, Def6

        .= ((the OFun of tfsm1 +* the OFun of tfsm2) . [(ad1 . k), (w . k)]) by A10, FUNCT_4: 11

        .= ((the OFun of tfsm1 +* the OFun of tfsm2) . [(((q,w) -admissible ) . k), (w . k)]) by A1, A2, A3, Th52

        .= (the OFun of tfsm . [(((q,w) -admissible ) . k), (w . k)]) by A1, Def24

        .= (res . k) by A8, Def6;

        hence (res1 . k) = (res . k);

      end;

      ( len res1) = ( len w) by Def6

      .= ( len res) by Def6;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: FSM_1:54

    

     Th54: tfsm = (tfsm1 -Mealy_union tfsm2) & q21 = q implies ((q21,w) -admissible ) = ((q,w) -admissible )

    proof

      set q9 = q21;

      assume that

       A1: tfsm = (tfsm1 -Mealy_union tfsm2) and

       A2: q9 = q;

      set ad9 = ((q9,w) -admissible ), ad = ((q,w) -admissible );

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len ad9) implies (ad9 . $1) = (ad . $1);

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: 1 <= k & k <= ( len ad9) implies (ad9 . k) = (ad . k);

        assume that 1 <= (k + 1) and

         A5: (k + 1) <= ( len ad9);

        

         A6: k = 0 or 0 < k & ( 0 + 1) = 1;

        per cases by A6, NAT_1: 13;

          suppose

           A7: k = 0 ;

          

          hence (ad9 . (k + 1)) = q9 by Def2

          .= (ad . (k + 1)) by A2, A7, Def2;

        end;

          suppose

           A8: 1 <= k;

          (k + 1) <= (( len w) + 1) by A5, Def2;

          then

           A9: k <= ( len w) by XREAL_1: 6;

          then

          consider w9k be Element of IAlph, q9k,q9k1 be Element of tfsm2 such that

           A10: w9k = (w . k) & q9k = (ad9 . k) and

           A11: q9k1 = (ad9 . (k + 1)) & (w9k -succ_of q9k) = q9k1 by A8, Def2;

          

           A12: ex wk be Element of IAlph, qk,qk1 be Element of tfsm st wk = (w . k) & qk = (ad . k) & qk1 = (ad . (k + 1)) & (wk -succ_of qk) = qk1 by A8, A9, Def2;

          ( len w) <= (( len w) + 1) by NAT_1: 11;

          then

           A13: k <= (( len w) + 1) by A9, XXREAL_0: 2;

          ( dom the Tran of tfsm2) = [:the carrier of tfsm2, IAlph:] by FUNCT_2:def 1;

          

          hence (ad9 . (k + 1)) = ((the Tran of tfsm1 +* the Tran of tfsm2) . [q9k, w9k]) by A11, FUNCT_4: 13

          .= (ad . (k + 1)) by A1, A4, A8, A10, A12, A13, Def2, Def24;

        end;

      end;

      

       A14: P[ 0 ];

      

       A15: for k be Nat holds P[k] from NAT_1:sch 2( A14, A3);

      ( len ad9) = (( len w) + 1) by Def2

      .= ( len ad) by Def2;

      hence thesis by A15, FINSEQ_1: 14;

    end;

    theorem :: FSM_1:55

    

     Th55: tfsm = (tfsm1 -Mealy_union tfsm2) & q21 = q implies ((q21,w) -response ) = ((q,w) -response )

    proof

      set q9 = q21;

      assume that

       A1: tfsm = (tfsm1 -Mealy_union tfsm2) and

       A2: q9 = q;

      set ad9 = ((q9,w) -admissible );

      set res = ((q,w) -response ), res9 = ((q9,w) -response );

      

       A3: ( len res9) = ( len w) by Def6;

       A4:

      now

        let k be Nat;

        assume 1 <= k & k <= ( len res9);

        then

         A5: k in ( Seg ( len w)) by A3, FINSEQ_1: 1;

        then

         A6: k in ( dom w) by FINSEQ_1:def 3;

        k in ( Seg (( len w) + 1)) by A5, FINSEQ_2: 8;

        then k in ( Seg ( len ad9)) by Def2;

        then k in ( dom ad9) by FINSEQ_1:def 3;

        then

         A7: (ad9 . k) in the carrier of tfsm2 by FINSEQ_2: 11;

        ( dom the OFun of tfsm2) = [:the carrier of tfsm2, IAlph:] & (w . k) in IAlph by A6, FINSEQ_2: 11, FUNCT_2:def 1;

        then

         A8: [(ad9 . k), (w . k)] in ( dom the OFun of tfsm2) by A7, ZFMISC_1: 87;

        (res9 . k) = (the OFun of tfsm2 . [(((q9,w) -admissible ) . k), (w . k)]) by A6, Def6

        .= ((the OFun of tfsm1 +* the OFun of tfsm2) . [(ad9 . k), (w . k)]) by A8, FUNCT_4: 13

        .= ((the OFun of tfsm1 +* the OFun of tfsm2) . [(((q,w) -admissible ) . k), (w . k)]) by A1, A2, Th54

        .= (the OFun of tfsm . [(((q,w) -admissible ) . k), (w . k)]) by A1, Def24

        .= (res . k) by A6, Def6;

        hence (res9 . k) = (res . k);

      end;

      ( len res9) = ( len w) by Def6

      .= ( len res) by Def6;

      hence thesis by A4, FINSEQ_1: 14;

    end;

    reserve Rtfsm1,Rtfsm2 for reduced non empty Mealy-FSM over IAlph, OAlph;

    theorem :: FSM_1:56

    

     Th56: tfsm = (Rtfsm1 -Mealy_union Rtfsm2) & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & (Rtfsm1,Rtfsm2) -are_equivalent implies ex Q be State of ( the_reduction_of tfsm) st the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of ( the_reduction_of tfsm)

    proof

      set rtfsm1 = Rtfsm1;

      set rtfsm2 = Rtfsm2;

      assume that

       A1: tfsm = (rtfsm1 -Mealy_union rtfsm2) and

       A2: the carrier of rtfsm1 misses the carrier of rtfsm2 and

       A3: (rtfsm1,rtfsm2) -are_equivalent ;

      set Srtfsm2 = the carrier of rtfsm2;

      set Stfsm = the carrier of tfsm, Srtfsm1 = the carrier of rtfsm1;

      Stfsm = (Srtfsm1 \/ Srtfsm2) by A1, Def24;

      then

      reconsider IS2 = the InitS of rtfsm2 as Element of Stfsm by XBOOLE_0:def 3;

      reconsider IS1 = the InitS of rtfsm1 as Element of Stfsm by A1, Def24;

      now

        let w be FinSequence of IAlph;

        ((the InitS of rtfsm1,w) -response ) = ((the InitS of rtfsm2,w) -response ) by A3;

        

        hence ((IS1,w) -response ) = ((the InitS of rtfsm2,w) -response ) by A1, A2, Th53

        .= ((IS2,w) -response ) by A1, Th55;

      end;

      then

       A4: (IS1,IS2) -are_equivalent ;

      set RUN = ( the_reduction_of tfsm);

      the InitS of tfsm = the InitS of rtfsm1 by A1, Def24;

      then

       A5: the InitS of rtfsm1 in the InitS of RUN by Def18;

      set SRUN = the carrier of RUN;

      

       A6: SRUN = ( final_states_partition tfsm) by Def18;

      ( final_states_partition tfsm) is final by Def15;

      then

      consider X be Element of SRUN such that

       A7: IS1 in X and

       A8: IS2 in X by A6, A4;

      take X;

      thus the InitS of rtfsm1 in X & the InitS of rtfsm2 in X by A7, A8;

      X is Subset of Stfsm & the InitS of RUN is Subset of Stfsm by A6, TARSKI:def 3;

      then X = the InitS of RUN or X misses the InitS of RUN by A6, EQREL_1:def 4;

      hence thesis by A7, A5, XBOOLE_0: 3;

    end;

    reserve CRtfsm1,CRtfsm2 for connected reduced non empty Mealy-FSM over IAlph, OAlph,

q1u,q2u for State of tfsm;

    theorem :: FSM_1:57

    

     Th57: for crq11,crq12 be State of CRtfsm1 holds crq11 = q1u & crq12 = q2u & the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = (CRtfsm1 -Mealy_union CRtfsm2) & not (crq11,crq12) -are_equivalent implies not (q1u,q2u) -are_equivalent

    proof

      let crq11,crq12 be State of CRtfsm1;

      set rtfsm1 = CRtfsm1, rtfsm2 = CRtfsm2, q1 = crq11, q2 = crq12;

      assume that

       A1: q1 = q1u and

       A2: q2 = q2u and

       A3: the carrier of rtfsm1 misses the carrier of rtfsm2 & tfsm = (rtfsm1 -Mealy_union rtfsm2);

      assume not (q1,q2) -are_equivalent ;

      then

      consider w be FinSequence of IAlph such that

       A4: ((q1,w) -response ) <> ((q2,w) -response );

      ((q1u,w) -response ) = ((q1,w) -response ) by A1, A3, Th53;

      then ((q1u,w) -response ) <> ((q2u,w) -response ) by A2, A3, A4, Th53;

      hence thesis;

    end;

    theorem :: FSM_1:58

    

     Th58: for crq21,crq22 be State of CRtfsm2 holds crq21 = q1u & crq22 = q2u & tfsm = (CRtfsm1 -Mealy_union CRtfsm2) & not (crq21,crq22) -are_equivalent implies not (q1u,q2u) -are_equivalent

    proof

      let crq21,crq22 be State of CRtfsm2;

      set rtfsm1 = CRtfsm1, rtfsm2 = CRtfsm2, q1 = crq21, q2 = crq22;

      assume that

       A1: q1 = q1u and

       A2: q2 = q2u and

       A3: tfsm = (rtfsm1 -Mealy_union rtfsm2);

      assume not (q1,q2) -are_equivalent ;

      then

      consider w be FinSequence of IAlph such that

       A4: ((q1,w) -response ) <> ((q2,w) -response );

      ((q1u,w) -response ) = ((q1,w) -response ) by A1, A3, Th55;

      then ((q1u,w) -response ) <> ((q2u,w) -response ) by A2, A3, A4, Th55;

      hence thesis;

    end;

    reserve CRtfsm1,CRtfsm2 for connected reduced finite non empty Mealy-FSM over IAlph, OAlph;

    theorem :: FSM_1:59

    

     Th59: the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = (CRtfsm1 -Mealy_union CRtfsm2) implies for Q be State of ( the_reduction_of tfsm) holds not ex q1,q2 be Element of Q st q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm1 & q1 <> q2

    proof

      set rtfsm1 = CRtfsm1;

      set rtfsm2 = CRtfsm2;

      assume that

       A1: the carrier of rtfsm1 misses the carrier of rtfsm2 and

       A2: tfsm = (rtfsm1 -Mealy_union rtfsm2);

      given Q be Element of ( the_reduction_of tfsm), q1,q2 be Element of Q such that

       A3: q1 in the carrier of rtfsm1 & q2 in the carrier of rtfsm1 and

       A4: q1 <> q2;

      consider tfsm1 be finite non empty Mealy-FSM over IAlph, OAlph such that

       A5: (rtfsm1,( the_reduction_of tfsm1)) -are_isomorphic by Th47;

      set tfsm1r = ( the_reduction_of tfsm1);

      consider Tf be Function of the carrier of rtfsm1, the carrier of tfsm1r such that

       A6: Tf is bijective and (Tf . the InitS of rtfsm1) = the InitS of tfsm1r and

       A7: for q be State of rtfsm1, s be Element of IAlph holds (Tf . (the Tran of rtfsm1 . (q,s))) = (the Tran of tfsm1r . ((Tf . q),s)) & (the OFun of rtfsm1 . (q,s)) = (the OFun of tfsm1r . ((Tf . q),s)) by A5;

      

       A8: ( dom Tf) = the carrier of rtfsm1 by FUNCT_2:def 1;

      then

       A9: (Tf . q1) <> (Tf . q2) by A3, A4, A6, FUNCT_1:def 4;

      ( rng Tf) = the carrier of tfsm1r by A6, FUNCT_2:def 3;

      then

      reconsider Tq1 = (Tf . q1), Tq2 = (Tf . q2) as Element of tfsm1r by A3, A8, FUNCT_1:def 3;

      the carrier of tfsm = (the carrier of rtfsm1 \/ the carrier of rtfsm2) by A2, Def24;

      then

      reconsider q1, q2 as Element of tfsm by A3, XBOOLE_0:def 3;

      reconsider q19 = q1, q29 = q2 as Element of rtfsm1 by A3;

       not (Tq1,Tq2) -are_equivalent by A9, Th45;

      then

       A10: not (q19,q29) -are_equivalent by A7, Th44;

      set rtfsm = ( the_reduction_of tfsm);

      

       A11: ( final_states_partition tfsm) is final by Def15;

      

       A12: the carrier of rtfsm = ( final_states_partition tfsm) by Def18;

      then

      reconsider Q as Subset of tfsm by TARSKI:def 3;

      (q1,q2) -are_equivalent by A11, A12;

      hence contradiction by A1, A2, A10, Th57;

    end;

    theorem :: FSM_1:60

    

     Th60: tfsm = (CRtfsm1 -Mealy_union CRtfsm2) implies for Q be State of ( the_reduction_of tfsm) holds not ex q1,q2 be Element of Q st q1 in the carrier of CRtfsm2 & q2 in the carrier of CRtfsm2 & q1 <> q2

    proof

      set rtfsm1 = CRtfsm1;

      set rtfsm2 = CRtfsm2;

      set rtfsm = ( the_reduction_of tfsm);

      consider tfsm2 be finite non empty Mealy-FSM over IAlph, OAlph such that

       A1: (rtfsm2,( the_reduction_of tfsm2)) -are_isomorphic by Th47;

      set tfsm2r = ( the_reduction_of tfsm2);

      consider Tf be Function of the carrier of rtfsm2, the carrier of tfsm2r such that

       A2: Tf is bijective and (Tf . the InitS of rtfsm2) = the InitS of tfsm2r and

       A3: for q be State of rtfsm2, s be Element of IAlph holds (Tf . (the Tran of rtfsm2 . (q,s))) = (the Tran of tfsm2r . ((Tf . q),s)) & (the OFun of rtfsm2 . (q,s)) = (the OFun of tfsm2r . ((Tf . q),s)) by A1;

      assume

       A4: tfsm = (rtfsm1 -Mealy_union rtfsm2);

      then

       A5: the carrier of tfsm = (the carrier of rtfsm1 \/ the carrier of rtfsm2) by Def24;

      given Q be Element of ( the_reduction_of tfsm), q1,q2 be Element of Q such that

       A6: q1 in the carrier of rtfsm2 and

       A7: q2 in the carrier of rtfsm2 and

       A8: q1 <> q2;

      

       A9: ( dom Tf) = the carrier of rtfsm2 by FUNCT_2:def 1;

      then

       A10: (Tf . q1) <> (Tf . q2) by A6, A7, A8, A2, FUNCT_1:def 4;

      ( rng Tf) = the carrier of tfsm2r by A2, FUNCT_2:def 3;

      then

      reconsider Tq1 = (Tf . q1), Tq2 = (Tf . q2) as Element of tfsm2r by A6, A7, A9, FUNCT_1:def 3;

      reconsider q2 as Element of tfsm by A7, A5, XBOOLE_0:def 3;

      reconsider q29 = q2 as Element of rtfsm2 by A7;

      reconsider q1 as Element of tfsm by A6, A5, XBOOLE_0:def 3;

      reconsider q19 = q1 as Element of rtfsm2 by A6;

       not (Tq1,Tq2) -are_equivalent by A10, Th45;

      then

       A11: not (q19,q29) -are_equivalent by A3, Th44;

      

       A12: the carrier of rtfsm = ( final_states_partition tfsm) by Def18;

      then

      reconsider Q as Subset of tfsm by TARSKI:def 3;

      

       A13: ( final_states_partition tfsm) is final by Def15;

      (q1,q2) -are_equivalent by A13, A12;

      hence contradiction by A4, A11, Th58;

    end;

    theorem :: FSM_1:61

    

     Th61: the carrier of CRtfsm1 misses the carrier of CRtfsm2 & (CRtfsm1,CRtfsm2) -are_equivalent & tfsm = (CRtfsm1 -Mealy_union CRtfsm2) implies for Q be State of ( the_reduction_of tfsm) holds ex q1,q2 be Element of Q st q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm2 & for q be Element of Q holds q = q1 or q = q2

    proof

      set rtfsm1 = CRtfsm1;

      set rtfsm2 = CRtfsm2;

      assume that

       A1: the carrier of rtfsm1 misses the carrier of rtfsm2 and

       A2: (rtfsm1,rtfsm2) -are_equivalent and

       A3: tfsm = (rtfsm1 -Mealy_union rtfsm2);

      set ISrtfsm2 = the InitS of rtfsm2;

      set ISrtfsm1 = the InitS of rtfsm1;

      

       A4: (the carrier of rtfsm1 /\ the carrier of rtfsm2) = {} by A1;

      set Stfsm = the carrier of tfsm;

      set Srtfsm2 = the carrier of rtfsm2;

      set Srtfsm1 = the carrier of rtfsm1;

      set rtfsm = ( the_reduction_of tfsm);

      set Srtfsm = the carrier of rtfsm;

      assume not thesis;

      then

      consider Q be Element of ( the_reduction_of tfsm) such that

       A5: for q1,q2 be Element of Q holds not q1 in the carrier of rtfsm1 or not q2 in the carrier of rtfsm2 or not for q be Element of Q holds q = q1 or q = q2;

      

       A6: Srtfsm = ( final_states_partition tfsm) by Def18;

      then

      reconsider Q as Subset of Stfsm by TARSKI:def 3;

      ( union ( final_states_partition tfsm)) = Stfsm by EQREL_1:def 4

      .= (Srtfsm1 \/ Srtfsm2) by A3, Def24;

      then

       A7: Q c= (Srtfsm1 \/ Srtfsm2) by A6, ZFMISC_1: 74;

      Q in Srtfsm;

      then

       A8: Q in ( final_states_partition tfsm) by Def18;

      then

       A9: Q <> {} ;

      then

      consider q be Element of Stfsm such that

       A10: q in Q by SUBSET_1: 4;

      per cases by A10, A7, XBOOLE_0:def 3;

        suppose

         A11: q in Srtfsm1;

        set Q9 = (Q \ {q});

         A12:

        now

          

           A13: Q9 c= Q by XBOOLE_1: 36;

          reconsider Q as Subset of Stfsm;

          assume

           A14: Q9 <> {} ;

          reconsider Q9 as Subset of Stfsm;

          consider x be Element of Stfsm such that

           A15: x in Q9 by A14, SUBSET_1: 4;

          

           A16: Q9 c= (Srtfsm1 \/ Srtfsm2) by A7, A13;

          per cases by A15, A16, XBOOLE_0:def 3;

            suppose

             A17: x in Srtfsm1;

            reconsider x as Element of Q by A15, XBOOLE_0:def 5;

            reconsider q as Element of Q by A10;

             not q in Srtfsm1 or not x in Srtfsm1 or q = x by A1, A3, Th59;

            hence contradiction by A11, A15, A17, ZFMISC_1: 56;

          end;

            suppose

             A18: x in Srtfsm2;

            set Q99 = (Q9 \ {x});

             A19:

            now

              

               A20: Q99 c= Q9 by XBOOLE_1: 36;

              reconsider Q9 as Subset of Stfsm;

              assume

               A21: Q99 <> {} ;

              reconsider Q99 as Subset of Stfsm;

              consider y be Element of Stfsm such that

               A22: y in Q99 by A21, SUBSET_1: 4;

              

               A23: Q99 c= (Srtfsm1 \/ Srtfsm2) by A16, A20;

              per cases by A22, A23, XBOOLE_0:def 3;

                suppose

                 A24: y in Srtfsm1;

                reconsider q as Element of Q by A10;

                

                 A25: y in Q9 by A22, ZFMISC_1: 56;

                then

                reconsider y as Element of Q by ZFMISC_1: 56;

                 not q in Srtfsm1 or not y in Srtfsm1 or q = y by A1, A3, Th59;

                hence contradiction by A11, A24, A25, ZFMISC_1: 56;

              end;

                suppose

                 A26: y in Srtfsm2;

                reconsider x as Element of Q by A15, ZFMISC_1: 56;

                y in Q9 by A22, ZFMISC_1: 56;

                then

                reconsider y as Element of Q by ZFMISC_1: 56;

                 not x in Srtfsm2 or not y in Srtfsm2 or x = y by A3, Th60;

                hence contradiction by A18, A22, A26, ZFMISC_1: 56;

              end;

            end;

            now

              assume

               A27: Q99 = {} ;

              

               A28: for z be Element of Q holds z = q or z = x

              proof

                given z be Element of Q such that

                 A29: z <> q and

                 A30: z <> x;

                z in Q9 by A9, A29, ZFMISC_1: 56;

                hence contradiction by A27, A30, ZFMISC_1: 56;

              end;

              reconsider x as Element of Q by A15, ZFMISC_1: 56;

              reconsider q as Element of Q by A10;

               not q in Srtfsm1 or not x in Srtfsm2 or ex z be Element of Q st z <> q & z <> x by A5;

              hence contradiction by A11, A18, A28;

            end;

            hence contradiction by A19;

          end;

        end;

        now

          reconsider q as Element of Srtfsm1 by A11;

          q is accessible by Def22;

          then

          consider w be FinSequence of IAlph such that

           A31: (ISrtfsm1,w) -leads_to q;

          set adl = (ISrtfsm2 leads_to_under w);

           A32:

          now

            reconsider q as Element of Stfsm;

            assume

             A33: not adl in Q;

            reconsider q1 = q as Element of Srtfsm1;

            adl in (Srtfsm1 \/ Srtfsm2) by XBOOLE_0:def 3;

            then

            reconsider adl as Element of Stfsm by A3, Def24;

            

             A34: not ex Y be Element of Srtfsm st q in Y & adl in Y

            proof

              reconsider Q as Subset of Stfsm;

              assume not thesis;

              then

              consider Y be Element of Srtfsm such that

               A35: q in Y and

               A36: adl in Y;

              reconsider Y as Subset of Stfsm by A6, TARSKI:def 3;

              Y in Srtfsm;

              then Y in ( final_states_partition tfsm) by Def18;

              then Y misses Q by A8, A33, A36, EQREL_1:def 4;

              hence contradiction by A10, A35, XBOOLE_0: 3;

            end;

            reconsider adl2 = adl as Element of Srtfsm2;

            ( final_states_partition tfsm) is final by Def15;

            then not (q,adl) -are_equivalent by A6, A34;

            then

            consider dseq be FinSequence of IAlph such that

             A37: ((q,dseq) -response ) <> ((adl,dseq) -response );

            ((q,dseq) -response ) = ((q1,dseq) -response ) by A1, A3, Th53;

            then

             A38: ((q1,dseq) -response ) <> ((adl2,dseq) -response ) by A3, A37, Th55;

            (ISrtfsm2,w) -leads_to adl2 by Def5;

            then ((ISrtfsm1,(w ^ dseq)) -response ) <> ((ISrtfsm2,(w ^ dseq)) -response ) by A31, A38, Th12;

            hence contradiction by A2;

          end;

          assume

           A39: Q9 = {} ;

          now

            assume

             A40: adl in Q;

            adl <> q by A4, XBOOLE_0:def 4;

            hence contradiction by A39, A40, ZFMISC_1: 56;

          end;

          hence contradiction by A32;

        end;

        hence contradiction by A12;

      end;

        suppose

         A41: q in Srtfsm2;

        set Q9 = (Q \ {q});

         A42:

        now

          

           A43: Q9 c= Q by XBOOLE_1: 36;

          reconsider Q as Subset of Stfsm;

          assume

           A44: Q9 <> {} ;

          reconsider Q9 as Subset of Stfsm;

          consider x be Element of Stfsm such that

           A45: x in Q9 by A44, SUBSET_1: 4;

          

           A46: Q9 c= (Srtfsm1 \/ Srtfsm2) by A7, A43;

          per cases by A45, A46, XBOOLE_0:def 3;

            suppose

             A47: x in Srtfsm1;

            set Q99 = (Q9 \ {x});

             A48:

            now

              

               A49: Q99 c= Q9 by XBOOLE_1: 36;

              reconsider Q9 as Subset of Stfsm;

              assume

               A50: Q99 <> {} ;

              reconsider Q99 as Subset of Stfsm;

              consider y be Element of Stfsm such that

               A51: y in Q99 by A50, SUBSET_1: 4;

              

               A52: Q99 c= (Srtfsm1 \/ Srtfsm2) by A46, A49;

              per cases by A51, A52, XBOOLE_0:def 3;

                suppose

                 A53: y in Srtfsm1;

                reconsider x as Element of Q by A45, ZFMISC_1: 56;

                y in Q9 by A51, ZFMISC_1: 56;

                then

                reconsider y as Element of Q by ZFMISC_1: 56;

                 not x in Srtfsm1 or not y in Srtfsm1 or x = y by A1, A3, Th59;

                hence contradiction by A47, A51, A53, ZFMISC_1: 56;

              end;

                suppose

                 A54: y in Srtfsm2;

                reconsider q as Element of Q by A10;

                

                 A55: y in Q9 by A51, ZFMISC_1: 56;

                then

                reconsider y as Element of Q by ZFMISC_1: 56;

                 not q in Srtfsm2 or not y in Srtfsm2 or q = y by A3, Th60;

                hence contradiction by A41, A54, A55, ZFMISC_1: 56;

              end;

            end;

            now

              assume

               A56: Q99 = {} ;

              

               A57: for z be Element of Q holds z = q or z = x

              proof

                given z be Element of Q such that

                 A58: z <> q and

                 A59: z <> x;

                z in Q9 by A9, A58, ZFMISC_1: 56;

                hence contradiction by A56, A59, ZFMISC_1: 56;

              end;

              reconsider x as Element of Q by A45, ZFMISC_1: 56;

              reconsider q as Element of Q by A10;

               not x in Srtfsm1 or not q in Srtfsm2 or ex z be Element of Q st z <> x & z <> q by A5;

              hence contradiction by A41, A47, A57;

            end;

            hence contradiction by A48;

          end;

            suppose

             A60: x in Srtfsm2;

            reconsider x as Element of Q by A45, XBOOLE_0:def 5;

            reconsider q as Element of Q by A10;

             not q in Srtfsm2 or not x in Srtfsm2 or q = x by A3, Th60;

            hence contradiction by A41, A45, A60, ZFMISC_1: 56;

          end;

        end;

        now

          reconsider q as Element of Srtfsm2 by A41;

          q is accessible by Def22;

          then

          consider w be FinSequence of IAlph such that

           A61: (ISrtfsm2,w) -leads_to q;

          set adl = (ISrtfsm1 leads_to_under w);

           A62:

          now

            reconsider q as Element of Stfsm;

            assume

             A63: not adl in Q;

            reconsider q1 = q as Element of Srtfsm2;

            adl in (Srtfsm1 \/ Srtfsm2) by XBOOLE_0:def 3;

            then

            reconsider adl as Element of Stfsm by A3, Def24;

            

             A64: not ex Y be Element of Srtfsm st q in Y & adl in Y

            proof

              assume not thesis;

              then

              consider Y be Element of Srtfsm such that

               A65: q in Y and

               A66: adl in Y;

              reconsider Y as Subset of Stfsm by A6, TARSKI:def 3;

              Y in Srtfsm;

              then Y in ( final_states_partition tfsm) by Def18;

              then Y misses Q by A8, A63, A66, EQREL_1:def 4;

              hence contradiction by A10, A65, XBOOLE_0: 3;

            end;

            reconsider adl2 = adl as Element of Srtfsm1;

            ( final_states_partition tfsm) is final by Def15;

            then not (q,adl) -are_equivalent by A6, A64;

            then

            consider dseq be FinSequence of IAlph such that

             A67: ((q,dseq) -response ) <> ((adl,dseq) -response );

            ((q,dseq) -response ) = ((q1,dseq) -response ) by A3, Th55;

            then

             A68: ((q1,dseq) -response ) <> ((adl2,dseq) -response ) by A1, A3, A67, Th53;

            (ISrtfsm1,w) -leads_to adl2 by Def5;

            then ((ISrtfsm2,(w ^ dseq)) -response ) <> ((ISrtfsm1,(w ^ dseq)) -response ) by A61, A68, Th12;

            hence contradiction by A2;

          end;

          assume

           A69: Q9 = {} ;

          now

            assume

             A70: adl in Q;

            adl <> q by A1, XBOOLE_0: 3;

            hence contradiction by A69, A70, ZFMISC_1: 56;

          end;

          hence contradiction by A62;

        end;

        hence contradiction by A42;

      end;

    end;

    begin

    theorem :: FSM_1:62

    

     Th62: for tfsm1,tfsm2 be finite non empty Mealy-FSM over IAlph, OAlph holds ex fsm1,fsm2 be finite non empty Mealy-FSM over IAlph, OAlph st the carrier of fsm1 misses the carrier of fsm2 & (fsm1,tfsm1) -are_isomorphic & (fsm2,tfsm2) -are_isomorphic

    proof

      deffunc F( object) = ($1 `2 );

      set z = 0 , zz = 1, A = {z}, B = {zz};

      let tfsm1,tfsm2 be finite non empty Mealy-FSM over IAlph, OAlph;

      set Stfsm1 = the carrier of tfsm1, Tr1 = the Tran of tfsm1;

      set Of1 = the OFun of tfsm1, Stfsm2 = the carrier of tfsm2;

      set Tr2 = the Tran of tfsm2, Of2 = the OFun of tfsm2;

      set Sfsm1 = [: { 0 }, Stfsm1:], Sfsm2 = [: {1}, Stfsm2:];

      deffunc F( Element of Sfsm1, Element of IAlph) = [($1 `1 ), (Tr1 . [($1 `2 ), $2])];

      consider T1 be Function of [:Sfsm1, IAlph:], Sfsm1 such that

       A1: for q be Element of Sfsm1, s be Element of IAlph holds (T1 . (q,s)) = F(q,s) from BINOP_1:sch 4;

      reconsider I2 = [1, the InitS of tfsm2] as Element of Sfsm2 by ZFMISC_1: 105;

      reconsider sSfsm2 = [:B, Stfsm2:] as finite non empty set;

      reconsider I1 = [ 0 , the InitS of tfsm1] as Element of Sfsm1 by ZFMISC_1: 105;

      set sSfsm1 = [:A, Stfsm1:];

      deffunc F( Element of Sfsm1, Element of IAlph) = (Of1 . [($1 `2 ), $2]);

      consider O1 be Function of [:Sfsm1, IAlph:], OAlph such that

       A2: for q be Element of Sfsm1, s be Element of IAlph holds (O1 . (q,s)) = F(q,s) from BINOP_1:sch 4;

      reconsider sI2 = I2 as Element of sSfsm2;

      set sI1 = I1;

      reconsider sO1 = O1 as Function of [:sSfsm1, IAlph:], OAlph;

      reconsider sT1 = T1 as Function of [:sSfsm1, IAlph:], sSfsm1;

      deffunc F( Element of Sfsm2, Element of IAlph) = [($1 `1 ), (Tr2 . [($1 `2 ), $2])];

      consider T2 be Function of [:Sfsm2, IAlph:], Sfsm2 such that

       A3: for q be Element of Sfsm2, s be Element of IAlph holds (T2 . (q,s)) = F(q,s) from BINOP_1:sch 4;

      reconsider sT2 = T2 as Function of [:sSfsm2, IAlph:], sSfsm2;

      take fsm1 = Mealy-FSM (# sSfsm1, sT1, sO1, sI1 #);

      deffunc F( Element of Sfsm2, Element of IAlph) = (Of2 . [($1 `2 ), $2]);

      consider O2 be Function of [:Sfsm2, IAlph:], OAlph such that

       A4: for q be Element of Sfsm2, s be Element of IAlph holds (O2 . (q,s)) = F(q,s) from BINOP_1:sch 4;

      

       A5: A misses B by ZFMISC_1: 11;

      reconsider sO2 = O2 as Function of [:sSfsm2, IAlph:], OAlph;

      take fsm2 = Mealy-FSM (# sSfsm2, sT2, sO2, sI2 #);

      (Sfsm1 /\ Sfsm2) = [:(A /\ B), (Stfsm1 /\ Stfsm2):] by ZFMISC_1: 100

      .= [: {} , (Stfsm1 /\ Stfsm2):] by A5

      .= {} by ZFMISC_1: 90;

      hence (the carrier of fsm1 /\ the carrier of fsm2) = {} ;

      thus (fsm1,tfsm1) -are_isomorphic

      proof

        deffunc F( object) = ($1 `2 );

        consider Tf1 be Function such that

         A6: ( dom Tf1) = the carrier of fsm1 & for q be object st q in the carrier of fsm1 holds (Tf1 . q) = F(q) from FUNCT_1:sch 3;

        

         A7: ( rng Tf1) = Stfsm1

        proof

          assume

           A8: not ( rng Tf1) = Stfsm1;

          per cases by A8;

            suppose not ( rng Tf1) c= Stfsm1;

            then

            consider q be object such that

             A9: q in ( rng Tf1) and

             A10: not q in Stfsm1;

            consider x be object such that

             A11: x in ( dom Tf1) and

             A12: q = (Tf1 . x) by A9, FUNCT_1:def 3;

            reconsider x2 = (x `2 ) as Element of Stfsm1 by A6, A11, MCART_1: 10;

            x2 in Stfsm1;

            hence contradiction by A6, A10, A11, A12;

          end;

            suppose not Stfsm1 c= ( rng Tf1);

            then

            consider x be object such that

             A13: x in Stfsm1 and

             A14: not x in ( rng Tf1);

             0 in { 0 } by TARSKI:def 1;

            then [ 0 , x] in sSfsm1 by A13, ZFMISC_1: 87;

            then (Tf1 . [ 0 , x]) in ( rng Tf1) & (Tf1 . [ 0 , x]) = ( [ 0 , x] `2 ) by A6, FUNCT_1:def 3;

            hence contradiction by A14;

          end;

        end;

        then

        reconsider Tf1s = Tf1 as Function of the carrier of fsm1, the carrier of tfsm1 by A6, FUNCT_2: 1;

        take Tf1s;

        now

          let x1,x2 be object;

          assume that

           A15: x1 in ( dom Tf1) and

           A16: x2 in ( dom Tf1) and

           A17: (Tf1 . x1) = (Tf1 . x2);

          

           A18: (Tf1 . x1) = (x1 `2 ) & (Tf1 . x2) = (x2 `2 ) by A6, A15, A16;

          (x1 `1 ) in A by A6, A15, MCART_1: 10;

          then

           A19: (x1 `1 ) = 0 by TARSKI:def 1;

          

           A20: (x2 `1 ) in A by A6, A16, MCART_1: 10;

          x1 = [(x1 `1 ), (x1 `2 )] & x2 = [(x2 `1 ), (x2 `2 )] by A6, A15, A16, MCART_1: 21;

          hence x1 = x2 by A17, A18, A20, A19, TARSKI:def 1;

        end;

        then Tf1s is one-to-one onto by A7, FUNCT_1:def 4, FUNCT_2:def 3;

        hence Tf1s is bijective;

        

        thus (Tf1s . the InitS of fsm1) = (sI1 `2 ) by A6

        .= the InitS of tfsm1;

        now

          let q be State of fsm1, s be Element of IAlph;

          reconsider q1 = (q `2 ) as Element of Stfsm1 by MCART_1: 10;

          reconsider Tq1 = (Tr1 . [q1, s]) as Element of Stfsm1;

          (q `1 ) in A by MCART_1: 10;

          then

           A21: [(q `1 ), Tq1] in [:A, Stfsm1:] by ZFMISC_1: 87;

          

          thus (Tf1s . (the Tran of fsm1 . (q,s))) = (Tf1s . ((q `1 ),(Tr1 . ((q `2 ),s)))) by A1

          .= ( [(q `1 ), (Tr1 . [(q `2 ), s])] `2 ) by A6, A21

          .= (Tr1 . [(q `2 ), s])

          .= (the Tran of tfsm1 . [(Tf1s . q), s]) by A6;

          

          thus (the OFun of fsm1 . (q,s)) = (Of1 . ((q `2 ),s)) by A2

          .= (the OFun of tfsm1 . ((Tf1s . q),s)) by A6;

        end;

        hence thesis;

      end;

      consider Tf1 be Function such that

       A22: ( dom Tf1) = the carrier of fsm2 & for q be object st q in the carrier of fsm2 holds (Tf1 . q) = F(q) from FUNCT_1:sch 3;

      

       A23: ( rng Tf1) = Stfsm2

      proof

        assume

         A24: not ( rng Tf1) = Stfsm2;

        per cases by A24;

          suppose not ( rng Tf1) c= Stfsm2;

          then

          consider q be object such that

           A25: q in ( rng Tf1) and

           A26: not q in Stfsm2;

          consider x be object such that

           A27: x in ( dom Tf1) and

           A28: q = (Tf1 . x) by A25, FUNCT_1:def 3;

          reconsider x2 = (x `2 ) as Element of Stfsm2 by A22, A27, MCART_1: 10;

          x2 in Stfsm2;

          hence contradiction by A22, A26, A27, A28;

        end;

          suppose not Stfsm2 c= ( rng Tf1);

          then

          consider x be object such that

           A29: x in Stfsm2 and

           A30: not x in ( rng Tf1);

          1 in {1} by TARSKI:def 1;

          then [1, x] in sSfsm2 by A29, ZFMISC_1: 87;

          then (Tf1 . [1, x]) in ( rng Tf1) & (Tf1 . [1, x]) = ( [1, x] `2 ) by A22, FUNCT_1:def 3;

          hence contradiction by A30;

        end;

      end;

      then

      reconsider Tf1s = Tf1 as Function of the carrier of fsm2, the carrier of tfsm2 by A22, FUNCT_2: 1;

      take Tf1s;

      now

        let x1,x2 be object;

        assume that

         A31: x1 in ( dom Tf1) and

         A32: x2 in ( dom Tf1) and

         A33: (Tf1 . x1) = (Tf1 . x2);

        

         A34: (Tf1 . x1) = (x1 `2 ) & (Tf1 . x2) = (x2 `2 ) by A22, A31, A32;

        (x1 `1 ) in B by A22, A31, MCART_1: 10;

        then

         A35: (x1 `1 ) = 1 by TARSKI:def 1;

        

         A36: (x2 `1 ) in B by A22, A32, MCART_1: 10;

        x1 = [(x1 `1 ), (x1 `2 )] & x2 = [(x2 `1 ), (x2 `2 )] by A22, A31, A32, MCART_1: 21;

        hence x1 = x2 by A33, A34, A36, A35, TARSKI:def 1;

      end;

      then Tf1s is one-to-one onto by A23, FUNCT_1:def 4, FUNCT_2:def 3;

      hence Tf1s is bijective;

      

      thus (Tf1s . the InitS of fsm2) = (sI2 `2 ) by A22

      .= the InitS of tfsm2;

      now

        let q be State of fsm2, s be Element of IAlph;

        reconsider q1 = (q `2 ) as Element of Stfsm2 by MCART_1: 10;

        set Tq1 = (Tr2 . [q1, s]);

        (q `1 ) in B by MCART_1: 10;

        then

         A37: [(q `1 ), Tq1] in [:B, Stfsm2:] by ZFMISC_1: 87;

        

        thus (Tf1s . (the Tran of fsm2 . (q,s))) = (Tf1s . ((q `1 ),(Tr2 . ((q `2 ),s)))) by A3

        .= ( [(q `1 ), (Tr2 . [(q `2 ), s])] `2 ) by A22, A37

        .= (Tr2 . [(q `2 ), s])

        .= (the Tran of tfsm2 . [(Tf1s . q), s]) by A22;

        

        thus (the OFun of fsm2 . (q,s)) = (Of2 . ((q `2 ),s)) by A4

        .= (the OFun of tfsm2 . [(Tf1s . q), s]) by A22;

      end;

      hence thesis;

    end;

    theorem :: FSM_1:63

    

     Th63: (tfsm1,tfsm2) -are_isomorphic implies (tfsm1,tfsm2) -are_equivalent

    proof

      assume (tfsm1,tfsm2) -are_isomorphic ;

      then

      consider Tf such that Tf is bijective and

       A1: (Tf . the InitS of tfsm1) = the InitS of tfsm2 and

       A2: for q be Element of tfsm1, s be Element of IAlph holds (Tf . (the Tran of tfsm1 . (q,s))) = (the Tran of tfsm2 . ((Tf . q),s)) & (the OFun of tfsm1 . (q,s)) = (the OFun of tfsm2 . ((Tf . q),s));

      now

        let w1 be FinSequence of IAlph;

        set rw1 = ((the InitS of tfsm1,w1) -response );

        set rw2 = ((the InitS of tfsm2,w1) -response );

        set aw1 = ((the InitS of tfsm1,w1) -admissible );

        set aw2 = ((the InitS of tfsm2,w1) -admissible );

        

         A3: for k be Nat st 1 <= k & k <= (( len w1) + 1) holds (Tf . (aw1 . k)) = (aw2 . k)

        proof

          defpred P[ Nat] means 1 <= $1 & $1 <= (( len w1) + 1) implies (Tf . (aw1 . $1)) = (aw2 . $1);

          

           A4: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A5: 1 <= k & k <= (( len w1) + 1) implies (Tf . (aw1 . k)) = (aw2 . k);

            assume that 1 <= (k + 1) and

             A6: (k + 1) <= (( len w1) + 1);

            

             A7: 0 = k or 0 < k & ( 0 + 1) = 1;

            per cases by A7, NAT_1: 13;

              suppose

               A8: 0 = k;

              

              hence (Tf . (aw1 . (k + 1))) = the InitS of tfsm2 by A1, Def2

              .= (aw2 . (k + 1)) by A8, Def2;

            end;

              suppose

               A9: 1 <= k;

              

               A10: ( len w1) <= (( len w1) + 1) by NAT_1: 11;

              

               A11: k <= ( len w1) by A6, XREAL_1: 6;

              then

              consider w1k be Element of IAlph, qk,qk1 be Element of tfsm1 such that

               A12: w1k = (w1 . k) & qk = (aw1 . k) and

               A13: qk1 = (aw1 . (k + 1)) & (w1k -succ_of qk) = qk1 by A9, Def2;

              consider w2k be Element of IAlph, q2k,q2k1 be Element of tfsm2 such that

               A14: w2k = (w1 . k) & q2k = (aw2 . k) and

               A15: q2k1 = (aw2 . (k + 1)) & (w2k -succ_of q2k) = q2k1 by A9, A11, Def2;

              

              thus (Tf . (aw1 . (k + 1))) = (Tf . (the Tran of tfsm1 . (qk,w1k))) by A13

              .= (the Tran of tfsm2 . (q2k,w2k)) by A2, A5, A9, A11, A12, A14, A10, XXREAL_0: 2

              .= (aw2 . (k + 1)) by A15;

            end;

          end;

          

           A16: P[ 0 ];

          thus for i be Nat holds P[i] from NAT_1:sch 2( A16, A4);

        end;

         A17:

        now

          let k be Nat;

          assume that

           A18: 1 <= k and

           A19: k <= ( len rw1);

          k <= ( len w1) by A19, Def6;

          then

           A20: k in ( dom w1) by A18, FINSEQ_3: 25;

          then

           A21: (w1 . k) is Element of IAlph by FINSEQ_2: 11;

          k in ( Seg ( len w1)) by A20, FINSEQ_1:def 3;

          then k in ( Seg (( len w1) + 1)) by FINSEQ_2: 8;

          then k in ( Seg ( len aw1)) by Def2;

          then

           A22: k in ( dom aw1) by FINSEQ_1:def 3;

          then

           A23: 1 <= k by FINSEQ_3: 25;

          k <= ( len aw1) by A22, FINSEQ_3: 25;

          then

           A24: k <= (( len w1) + 1) by Def2;

          

           A25: (aw1 . k) is Element of tfsm1 by A22, FINSEQ_2: 11;

          

          thus (rw2 . k) = (the OFun of tfsm2 . [(aw2 . k), (w1 . k)]) by A20, Def6

          .= (the OFun of tfsm2 . ((Tf . (aw1 . k)),(w1 . k))) by A3, A23, A24

          .= (the OFun of tfsm1 . ((aw1 . k),(w1 . k))) by A2, A25, A21

          .= (rw1 . k) by A20, Def6;

        end;

        ( len rw1) = ( len w1) by Def6

        .= ( len rw2) by Def6;

        hence rw1 = rw2 by A17, FINSEQ_1: 14;

      end;

      hence thesis;

    end;

    theorem :: FSM_1:64

    

     Th64: the carrier of CRtfsm1 misses the carrier of CRtfsm2 & (CRtfsm1,CRtfsm2) -are_equivalent implies (CRtfsm1,CRtfsm2) -are_isomorphic

    proof

      set rtfsm1 = CRtfsm1;

      set rtfsm2 = CRtfsm2;

      assume that

       A1: the carrier of rtfsm1 misses the carrier of rtfsm2 and

       A2: (rtfsm1,rtfsm2) -are_equivalent ;

      set Srtfsm2 = the carrier of rtfsm2;

      set Srtfsm1 = the carrier of rtfsm1;

      set UN = (rtfsm1 -Mealy_union rtfsm2);

      set RUN = ( the_reduction_of UN);

      set SRUN = the carrier of RUN;

      defpred P[ object, object] means ex part be Element of SRUN st $1 in part & $2 in (part \ {$1});

      

       A3: SRUN = ( final_states_partition UN) by Def18;

      

       A4: for x be object st x in Srtfsm1 holds ex y be object st P[x, y]

      proof

        let x be object;

        set xs = {x};

        

         A5: ( union SRUN) = the carrier of UN by A3, EQREL_1:def 4;

        assume

         A6: x in Srtfsm1;

        then x in (Srtfsm1 \/ Srtfsm2) by XBOOLE_0:def 3;

        then x in the carrier of UN by Def24;

        then

        consider part be set such that

         A7: x in part and

         A8: part in SRUN by A5, TARSKI:def 4;

        reconsider part as Element of SRUN by A8;

        consider p,y be Element of part such that p in Srtfsm1 and

         A9: y in Srtfsm2 and for z be Element of part holds z = p or z = y by A1, A2, Th61;

        set IT = y;

        take IT;

        x <> y by A1, A6, A9, XBOOLE_0: 3;

        then y in (part \ xs) by A7, ZFMISC_1: 56;

        hence thesis by A7;

      end;

      consider f be Function such that

       A10: ( dom f) = Srtfsm1 & for x be object st x in Srtfsm1 holds P[x, (f . x)] from CLASSES1:sch 1( A4);

      now

        assume

         A11: not ( rng f) c= Srtfsm2 or not Srtfsm2 c= ( rng f);

        per cases by A11;

          suppose not ( rng f) c= Srtfsm2;

          then

          consider y1 be object such that

           A12: y1 in ( rng f) and

           A13: not y1 in Srtfsm2;

          consider x1 be object such that

           A14: x1 in Srtfsm1 and

           A15: y1 = (f . x1) by A10, A12, FUNCT_1:def 3;

          consider part1 be Element of SRUN such that

           A16: x1 in part1 and

           A17: (f . x1) in (part1 \ {x1}) by A10, A14;

           A18:

          now

            assume

             A19: y1 in Srtfsm1;

            y1 <> x1 by A15, A17, ZFMISC_1: 56;

            hence contradiction by A1, A14, A15, A16, A17, A19, Th59;

          end;

          part1 is Subset of UN by A3, TARSKI:def 3;

          then

           A20: part1 is Subset of (Srtfsm1 \/ Srtfsm2) by Def24;

          y1 in part1 by A15, A17;

          hence contradiction by A13, A20, A18, XBOOLE_0:def 3;

        end;

          suppose

           A21: not Srtfsm2 c= ( rng f);

          

           A22: ( union SRUN) = the carrier of UN by A3, EQREL_1:def 4;

          consider y1 be object such that

           A23: y1 in Srtfsm2 and

           A24: not y1 in ( rng f) by A21;

          y1 in (Srtfsm1 \/ Srtfsm2) by A23, XBOOLE_0:def 3;

          then y1 in the carrier of UN by Def24;

          then

          consider Z be set such that

           A25: y1 in Z and

           A26: Z in SRUN by A22, TARSKI:def 4;

          reconsider Z as Element of SRUN by A26;

          

           A27: Z is Subset of UN by A3, TARSKI:def 3;

          consider q1,q2 be Element of Z such that

           A28: q1 in Srtfsm1 and q2 in Srtfsm2 and for q be Element of Z holds q = q1 or q = q2 by A1, A2, Th61;

          consider F be Element of SRUN such that

           A29: q1 in F and

           A30: (f . q1) in (F \ {q1}) by A10, A28;

          F is Subset of UN by A3, TARSKI:def 3;

          then

           A31: Z = F or Z misses F by A3, A27, EQREL_1:def 4;

          

           A32: (f . q1) in F by A30;

          now

             A33:

            now

              assume

               A34: (f . q1) in Srtfsm1;

              (f . q1) <> q1 by A30, ZFMISC_1: 56;

              hence contradiction by A1, A28, A29, A30, A34, Th59;

            end;

            Z is Subset of (Srtfsm1 \/ Srtfsm2) by A27, Def24;

            then

             A35: (f . q1) in Srtfsm1 or (f . q1) in Srtfsm2 by A25, A29, A31, A32, XBOOLE_0: 3, XBOOLE_0:def 3;

            assume y1 <> (f . q1);

            hence contradiction by A23, A25, A29, A30, A31, A35, A33, Th60, XBOOLE_0: 3;

          end;

          hence contradiction by A10, A24, A28, FUNCT_1:def 3;

        end;

      end;

      then

       A36: ( rng f) = Srtfsm2;

       A37:

      now

        let x1,x2 be object;

        assume that

         A38: x1 in ( dom f) and

         A39: x2 in ( dom f) and

         A40: (f . x1) = (f . x2);

        consider part1 be Element of SRUN such that

         A41: x1 in part1 & (f . x1) in (part1 \ {x1}) by A10, A38;

        consider part2 be Element of SRUN such that

         A42: x2 in part2 & (f . x2) in (part2 \ {x2}) by A10, A39;

        assume

         A43: x1 <> x2;

        part1 is Subset of UN & part2 is Subset of UN by A3, TARSKI:def 3;

        then part1 = part2 or part1 misses part2 by A3, EQREL_1:def 4;

        hence contradiction by A1, A10, A38, A39, A40, A43, A41, A42, Th59, XBOOLE_0: 3;

      end;

      reconsider f as Function of Srtfsm1, Srtfsm2 by A10, A36, FUNCT_2: 1;

      

       A44: (f . the InitS of rtfsm1) = the InitS of rtfsm2

      proof

        consider part be Element of SRUN such that

         A45: the InitS of rtfsm1 in part & (f . the InitS of rtfsm1) in (part \ {the InitS of rtfsm1}) by A10;

        consider Q be Element of SRUN such that

         A46: the InitS of rtfsm1 in Q & the InitS of rtfsm2 in Q and Q = the InitS of RUN by A1, A2, Th56;

        assume

         A47: (f . the InitS of rtfsm1) <> the InitS of rtfsm2;

        Q is Subset of UN & part is Subset of UN by A3, TARSKI:def 3;

        then Q = part or Q misses part by A3, EQREL_1:def 4;

        hence contradiction by A47, A46, A45, Th60, XBOOLE_0: 3;

      end;

      

       A48: for q be State of rtfsm1, s be Element of IAlph holds (f . (the Tran of rtfsm1 . (q,s))) = (the Tran of rtfsm2 . ((f . q),s)) & (the OFun of rtfsm1 . (q,s)) = (the OFun of rtfsm2 . ((f . q),s))

      proof

        let q be State of rtfsm1, s be Element of IAlph;

        set q1 = (the Tran of rtfsm1 . [q, s]), fq = (f . q);

        set q2 = (the Tran of rtfsm2 . [fq, s]);

        

         A49: ( dom the Tran of rtfsm2) = [:Srtfsm2, IAlph:] by FUNCT_2:def 1;

        

         A50: the carrier of UN = (Srtfsm1 \/ Srtfsm2) by Def24;

        then

        reconsider q9 = q as Element of UN by XBOOLE_0:def 3;

        (f . q) in ( rng f) by A10, FUNCT_1:def 3;

        then

        reconsider fq9 = (f . q9) as Element of UN by A50, XBOOLE_0:def 3;

        set qu = (the Tran of UN . [q9, s]), qfu = (the Tran of UN . [fq9, s]);

        

         A51: qfu = ((the Tran of rtfsm1 +* the Tran of rtfsm2) . [fq9, s]) by Def24

        .= q2 by A49, FUNCT_4: 13;

        consider XX be Element of SRUN such that

         A52: q1 in XX & (f . q1) in (XX \ {q1}) by A10;

        

         A53: ( final_states_partition UN) is final by Def15;

        ex part be Element of SRUN st q in part & (f . q) in (part \ {q}) by A10;

        then

         A54: (q9,fq9) -are_equivalent by A3, A53;

        then (qu,qfu) -are_equivalent by Th19;

        then

        consider X be Element of SRUN such that

         A55: qu in X & qfu in X by A3, A53;

        

         A56: (the carrier of rtfsm1 /\ the carrier of rtfsm2) = {} by A1;

        

         A57: ( dom the Tran of rtfsm1) = [:Srtfsm1, IAlph:] by FUNCT_2:def 1;

        

        then (( dom the Tran of rtfsm1) /\ ( dom the Tran of rtfsm2)) = ( [:Srtfsm1, IAlph:] /\ [:Srtfsm2, IAlph:]) by FUNCT_2:def 1

        .= [: {} , IAlph:] by A56, ZFMISC_1: 99

        .= {} by ZFMISC_1: 90;

        then

         A58: ( dom the Tran of rtfsm1) misses ( dom the Tran of rtfsm2);

        

         A59: qu = ((the Tran of rtfsm1 +* the Tran of rtfsm2) . [q9, s]) by Def24

        .= q1 by A57, A58, FUNCT_4: 16;

        

         A60: X is Subset of UN by A3, TARSKI:def 3;

        now

          XX is Subset of UN by A3, TARSKI:def 3;

          then

           A61: X = XX or X misses XX by A3, A60, EQREL_1:def 4;

          assume (f . q1) <> q2;

          hence contradiction by A55, A59, A51, A52, A61, Th60, XBOOLE_0: 3;

        end;

        hence (f . (the Tran of rtfsm1 . (q,s))) = (the Tran of rtfsm2 . ((f . q),s));

        

         A62: ( dom the OFun of rtfsm2) = [:Srtfsm2, IAlph:] by FUNCT_2:def 1;

        

         A63: ( dom the OFun of rtfsm1) = [:Srtfsm1, IAlph:] by FUNCT_2:def 1;

        

        then (( dom the OFun of rtfsm1) /\ ( dom the OFun of rtfsm2)) = [:(Srtfsm1 /\ Srtfsm2), IAlph:] by A62, ZFMISC_1: 99

        .= {} by A56, ZFMISC_1: 90;

        then ( dom the OFun of rtfsm1) misses ( dom the OFun of rtfsm2);

        

        hence (the OFun of rtfsm1 . (q,s)) = ((the OFun of rtfsm1 +* the OFun of rtfsm2) . [q, s]) by A63, FUNCT_4: 16

        .= (the OFun of UN . [q9, s]) by Def24

        .= (the OFun of UN . [fq9, s]) by A54, Th19

        .= ((the OFun of rtfsm1 +* the OFun of rtfsm2) . [(f . q), s]) by Def24

        .= (the OFun of rtfsm2 . ((f . q),s)) by A62, FUNCT_4: 13;

      end;

      f is one-to-one onto by A37, A36, FUNCT_1:def 4, FUNCT_2:def 3;

      hence thesis by A44, A48;

    end;

    theorem :: FSM_1:65

    

     Th65: (Ctfsm1,Ctfsm2) -are_equivalent implies (( the_reduction_of Ctfsm1),( the_reduction_of Ctfsm2)) -are_isomorphic

    proof

      assume

       A1: (Ctfsm1,Ctfsm2) -are_equivalent ;

      set rtfsm2 = ( the_reduction_of Ctfsm2);

      set rtfsm1 = ( the_reduction_of Ctfsm1);

      consider fsm1,fsm2 be finite non empty Mealy-FSM over IAlph, OAlph such that

       A2: the carrier of fsm1 misses the carrier of fsm2 and

       A3: (fsm1,rtfsm1) -are_isomorphic and

       A4: (fsm2,rtfsm2) -are_isomorphic by Th62;

      

       A5: (rtfsm1,Ctfsm1) -are_equivalent by Th41;

      set Srtfsm1 = the carrier of rtfsm1, Srtfsm2 = the carrier of rtfsm2;

      set ISrtfsm1 = the InitS of rtfsm1, ISrtfsm2 = the InitS of rtfsm2;

      set Sfsm1 = the carrier of fsm1, Sfsm2 = the carrier of fsm2;

      set ISfsm1 = the InitS of fsm1, ISfsm2 = the InitS of fsm2;

      

       A6: (rtfsm2,Ctfsm2) -are_equivalent by Th41;

      (fsm2,rtfsm2) -are_equivalent by A4, Th63;

      then

       A7: (fsm2,Ctfsm2) -are_equivalent by A6, Th15;

      

       A8: fsm1 is connected

      proof

        assume not fsm1 is connected;

        then

        consider q1 be Element of Sfsm1 such that

         A9: not q1 is accessible;

        consider Tf be Function of the carrier of fsm1, Srtfsm1 such that

         A10: Tf is bijective and

         A11: (Tf . the InitS of fsm1) = ISrtfsm1 & for q be State of fsm1, s be Element of IAlph holds (Tf . (the Tran of fsm1 . (q,s))) = (the Tran of rtfsm1 . ((Tf . q),s)) & (the OFun of fsm1 . (q,s)) = (the OFun of rtfsm1 . ((Tf . q),s)) by A3;

        

         A12: ( dom Tf) = Sfsm1 by FUNCT_2:def 1;

        set q = (Tf . q1);

        q is accessible by Def22;

        then

        consider w be FinSequence of IAlph such that

         A13: (ISrtfsm1,w) -leads_to q;

        

         A14: 1 <= (( len w) + 1) by NAT_1: 11;

        then (Tf . (((ISfsm1,w) -admissible ) . (( len w) + 1))) = (((ISrtfsm1,w) -admissible ) . (( len w) + 1)) by A11, Th43;

        then

         A15: ((Tf " ) . (Tf . (((ISfsm1,w) -admissible ) . (( len w) + 1)))) = ((Tf " ) . q) by A13;

        ( len ((ISfsm1,w) -admissible )) = (( len w) + 1) by Def2;

        then (( len w) + 1) in ( Seg ( len ((ISfsm1,w) -admissible ))) by A14, FINSEQ_1: 1;

        then (( len w) + 1) in ( dom ((ISfsm1,w) -admissible )) by FINSEQ_1:def 3;

        then (((the InitS of fsm1,w) -admissible ) . (( len w) + 1)) in ( dom Tf) by A12, FINSEQ_2: 11;

        

        then (((ISfsm1,w) -admissible ) . (( len w) + 1)) = ((Tf " ) . (Tf . q1)) by A10, A15, FUNCT_1: 34

        .= q1 by A10, A12, FUNCT_1: 34;

        then (ISfsm1,w) -leads_to q1;

        hence contradiction by A9;

      end;

      

       A16: fsm2 is connected

      proof

        assume not fsm2 is connected;

        then

        consider q1 be Element of Sfsm2 such that

         A17: not q1 is accessible;

        consider Tf be Function of Sfsm2, Srtfsm2 such that

         A18: Tf is bijective and

         A19: (Tf . ISfsm2) = ISrtfsm2 & for q be State of fsm2, s be Element of IAlph holds (Tf . (the Tran of fsm2 . (q,s))) = (the Tran of rtfsm2 . ((Tf . q),s)) & (the OFun of fsm2 . (q,s)) = (the OFun of rtfsm2 . ((Tf . q),s)) by A4;

        

         A20: ( dom Tf) = Sfsm2 by FUNCT_2:def 1;

        set q = (Tf . q1);

        q is accessible by Def22;

        then

        consider w be FinSequence of IAlph such that

         A21: (ISrtfsm2,w) -leads_to q;

        

         A22: 1 <= (( len w) + 1) by NAT_1: 11;

        then (Tf . (((ISfsm2,w) -admissible ) . (( len w) + 1))) = (((ISrtfsm2,w) -admissible ) . (( len w) + 1)) by A19, Th43;

        then

         A23: ((Tf " ) . (Tf . (((ISfsm2,w) -admissible ) . (( len w) + 1)))) = ((Tf " ) . q) by A21;

        ( len ((ISfsm2,w) -admissible )) = (( len w) + 1) by Def2;

        then (( len w) + 1) in ( Seg ( len ((ISfsm2,w) -admissible ))) by A22, FINSEQ_1: 1;

        then (( len w) + 1) in ( dom ((ISfsm2,w) -admissible )) by FINSEQ_1:def 3;

        then (((ISfsm2,w) -admissible ) . (( len w) + 1)) in ( dom Tf) by A20, FINSEQ_2: 11;

        

        then (((ISfsm2,w) -admissible ) . (( len w) + 1)) = ((Tf " ) . (Tf . q1)) by A18, A23, FUNCT_1: 34

        .= q1 by A18, A20, FUNCT_1: 34;

        then (ISfsm2,w) -leads_to q1;

        hence contradiction by A17;

      end;

      (fsm1,rtfsm1) -are_equivalent by A3, Th63;

      then (fsm1,Ctfsm1) -are_equivalent by A5, Th15;

      then

       A24: (fsm1,Ctfsm2) -are_equivalent by A1, Th15;

      reconsider fsm1, fsm2 as reduced finite non empty Mealy-FSM over IAlph, OAlph by A3, A4, Th47;

      (fsm1,fsm2) -are_isomorphic by A2, A8, A16, A7, A24, Th15, Th64;

      then (fsm1,rtfsm2) -are_isomorphic by A4, Th42;

      hence thesis by A3, Th42;

    end;

    ::$Notion-Name

    theorem :: FSM_1:66

    for M1,M2 be connected reduced finite non empty Mealy-FSM over IAlph, OAlph holds (M1,M2) -are_isomorphic iff (M1,M2) -are_equivalent

    proof

      let M1,M2 be connected reduced finite non empty Mealy-FSM over IAlph, OAlph;

      thus (M1,M2) -are_isomorphic implies (M1,M2) -are_equivalent by Th63;

      

       A1: (M2,( the_reduction_of M2)) -are_isomorphic by Th46;

      assume (M1,M2) -are_equivalent ;

      then

       A2: (( the_reduction_of M1),( the_reduction_of M2)) -are_isomorphic by Th65;

      (M1,( the_reduction_of M1)) -are_isomorphic by Th46;

      then (M1,( the_reduction_of M2)) -are_isomorphic by A2, Th42;

      hence thesis by A1, Th42;

    end;