fsm_2.miz



    begin

    reserve x,y for Real,

i,j for non zero Element of NAT ,

I,O for non empty set,

s,s1,s2,s3 for Element of I,

w,w1,w2 for FinSequence of I,

t for Element of O,

S for non empty FSM over I,

q,q1 for State of S;

    notation

      let I, S, q, w;

      synonym GEN (w,q) for (q,w) -admissible ;

    end

    registration

      let I, S, q, w;

      cluster ( GEN (w,q)) -> non empty;

      coherence

      proof

        ( len ( GEN (w,q))) = (( len w) + 1) by FSM_1:def 2;

        hence thesis;

      end;

    end

    theorem :: FSM_2:1

    

     Th1: ( GEN ( <*s*>,q)) = <*q, (the Tran of S . [q, s])*>

    proof

      

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

      

       A2: ( len ( GEN ( <*s*>,q))) = (( len <*s*>) + 1) by FSM_1:def 2

      .= 2 by A1;

      

       A3: (( GEN ( <*s*>,q)) . 1) = q by FSM_1:def 2;

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

      then

      consider WI be Element of I, QI,QI1 be State of S such that

       A4: WI = ( <*s*> . 1) and

       A5: QI = (( GEN ( <*s*>,q)) . 1) and

       A6: QI1 = (( GEN ( <*s*>,q)) . (1 + 1)) and

       A7: (WI -succ_of QI) = QI1 by FSM_1:def 2;

      WI = s by A4, FINSEQ_1: 40;

      hence thesis by A2, A3, A5, A6, A7, FINSEQ_1: 44;

    end;

    theorem :: FSM_2:2

    

     Th2: ( GEN ( <*s1, s2*>,q)) = <*q, (the Tran of S . [q, s1]), (the Tran of S . [(the Tran of S . [q, s1]), s2])*>

    proof

      set w = <*s1, s2*>;

      

       A1: (( GEN (w,q)) . 1) = q by FSM_1:def 2;

      

       A2: w = ( <*s1*> ^ <*s2*>) by FINSEQ_1:def 9;

      

       A3: ( len <*s1*>) = 1 by FINSEQ_1: 39;

      ( GEN ( <*s1*>,q)) = <*q, (the Tran of S . [q, s1])*> by Th1;

      then (( GEN ( <*s1*>,q)) . (1 + 1)) = (the Tran of S . [q, s1]) by FINSEQ_1: 44;

      then (q, <*s1*>) -leads_to (the Tran of S . [q, s1]) by A3;

      then

       A4: (( GEN (w,q)) . (1 + 1)) = (the Tran of S . [q, s1]) by A2, A3, FSM_1: 6;

      

       A5: ( len w) = 2 by FINSEQ_1: 44;

      2 <= ( len w) by FINSEQ_1: 44;

      then

      consider WI be Element of I, QI,QI1 be State of S such that

       A6: WI = (w . 2) and

       A7: QI = (( GEN (w,q)) . 2) and

       A8: QI1 = (( GEN (w,q)) . (2 + 1)) and

       A9: (WI -succ_of QI) = QI1 by FSM_1:def 2;

      

       A10: WI = s2 by A6, FINSEQ_1: 44;

      ( len ( GEN (w,q))) = (( len w) + 1) by FSM_1:def 2

      .= 3 by A5;

      hence thesis by A1, A4, A7, A8, A9, A10, FINSEQ_1: 45;

    end;

    theorem :: FSM_2:3

    ( GEN ( <*s1, s2, s3*>,q)) = <*q, (the Tran of S . [q, s1]), (the Tran of S . [(the Tran of S . [q, s1]), s2]), (the Tran of S . [(the Tran of S . [(the Tran of S . [q, s1]), s2]), s3])*>

    proof

      set w = <*s1, s2, s3*>;

      reconsider w1 = <*s1, s2*>, w2 = <*s3*> as FinSequence of I;

      set Q = (the Tran of S . [(the Tran of S . [q, s1]), s2]);

      

       A1: w = (w1 ^ w2) by FINSEQ_1: 43;

      

       A2: ( len w1) = 2 by FINSEQ_1: 44;

      ( GEN (w1,q)) = <*q, (the Tran of S . [q, s1]), Q*> by Th2;

      then (( GEN (w1,q)) . (( len w1) + 1)) = Q by A2, FINSEQ_1: 45;

      then (q,w1) -leads_to Q;

      then

       A3: ( GEN (w,q)) = (( Del (( GEN (w1,q)),(( len w1) + 1))) ^ ( GEN (w2,Q))) by A1, FSM_1: 8;

      ( Del (( GEN (w1,q)),(( len w1) + 1))) = ( Del ( <*q, (the Tran of S . [q, s1]), Q*>,3)) by A2, Th2

      .= <*q, (the Tran of S . [q, s1])*> by WSIERP_1: 19;

      then ( GEN (w,q)) = ( <*q, (the Tran of S . [q, s1])*> ^ <*Q, (the Tran of S . [Q, s3])*>) by A3, Th1;

      hence thesis by FINSEQ_4: 74;

    end;

    definition

      let I, S;

      :: FSM_2:def1

      attr S is calculating_type means for j holds for w1, w2 st (w1 . 1) = (w2 . 1) & j <= (( len w1) + 1) & j <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . j) = (( GEN (w2,the InitS of S)) . j);

    end

    theorem :: FSM_2:4

    

     Th4: S is calculating_type implies for w1, w2 st (w1 . 1) = (w2 . 1) holds (( GEN (w1,the InitS of S)),( GEN (w2,the InitS of S))) are_c=-comparable

    proof

      assume

       A1: S is calculating_type;

      let w1, w2 such that

       A2: (w1 . 1) = (w2 . 1);

      set A = (( Seg (1 + ( len w1))) /\ ( Seg (1 + ( len w2))));

      (1 + ( len w1)) <= (1 + ( len w2)) or (1 + ( len w2)) <= (1 + ( len w1));

      then

       A3: ( Seg (1 + ( len w1))) c= ( Seg (1 + ( len w2))) & A = ( Seg (1 + ( len w1))) or ( Seg (1 + ( len w2))) c= ( Seg (1 + ( len w1))) & A = ( Seg (1 + ( len w2))) by FINSEQ_1: 5, FINSEQ_1: 7;

      

       A4: ( len ( GEN (w1,the InitS of S))) = (1 + ( len w1)) by FSM_1:def 2;

      

       A5: ( len ( GEN (w2,the InitS of S))) = (1 + ( len w2)) by FSM_1:def 2;

      

       A6: ( dom ( GEN (w1,the InitS of S))) = ( Seg (1 + ( len w1))) by A4, FINSEQ_1:def 3;

      

       A7: ( dom ( GEN (w2,the InitS of S))) = ( Seg (1 + ( len w2))) by A5, FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A8: x in A;

        then

        reconsider i = x as Element of NAT ;

        

         A9: i >= 1 by A3, A8, FINSEQ_1: 1;

        

         A10: i <= (1 + ( len w1)) by A3, A8, FINSEQ_1: 1;

        i <= (1 + ( len w2)) by A3, A8, FINSEQ_1: 1;

        hence (( GEN (w1,the InitS of S)) . x) = (( GEN (w2,the InitS of S)) . x) by A1, A2, A9, A10;

      end;

      hence ( GEN (w1,the InitS of S)) c= ( GEN (w2,the InitS of S)) or ( GEN (w2,the InitS of S)) c= ( GEN (w1,the InitS of S)) by A3, A6, A7, GRFUNC_1: 2;

    end;

    theorem :: FSM_2:5

    

     Th5: (for w1, w2 st (w1 . 1) = (w2 . 1) holds (( GEN (w1,the InitS of S)),( GEN (w2,the InitS of S))) are_c=-comparable ) implies S is calculating_type

    proof

      assume

       A1: for w1, w2 st (w1 . 1) = (w2 . 1) holds (( GEN (w1,the InitS of S)),( GEN (w2,the InitS of S))) are_c=-comparable ;

      let j, w1, w2 such that

       A2: (w1 . 1) = (w2 . 1) and

       A3: j <= (( len w1) + 1) and

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

      

       A5: ( dom ( GEN (w1,the InitS of S))) = ( Seg ( len ( GEN (w1,the InitS of S)))) by FINSEQ_1:def 3

      .= ( Seg (( len w1) + 1)) by FSM_1:def 2;

      

       A6: ( dom ( GEN (w2,the InitS of S))) = ( Seg ( len ( GEN (w2,the InitS of S)))) by FINSEQ_1:def 3

      .= ( Seg (( len w2) + 1)) by FSM_1:def 2;

      

       A7: 1 <= j by NAT_1: 14;

      then

       A8: j in ( dom ( GEN (w1,the InitS of S))) by A3, A5, FINSEQ_1: 1;

      j in ( dom ( GEN (w2,the InitS of S))) by A4, A6, A7, FINSEQ_1: 1;

      then

       A9: j in (( dom ( GEN (w1,the InitS of S))) /\ ( dom ( GEN (w2,the InitS of S)))) by A8, XBOOLE_0:def 4;

      (( GEN (w1,the InitS of S)),( GEN (w2,the InitS of S))) are_c=-comparable by A1, A2;

      then ( GEN (w1,the InitS of S)) c= ( GEN (w2,the InitS of S)) or ( GEN (w2,the InitS of S)) c= ( GEN (w1,the InitS of S));

      then ( GEN (w1,the InitS of S)) tolerates ( GEN (w2,the InitS of S)) by PARTFUN1: 54;

      hence thesis by A9, PARTFUN1:def 4;

    end;

    theorem :: FSM_2:6

    S is calculating_type implies for w1, w2 st (w1 . 1) = (w2 . 1) & ( len w1) = ( len w2) holds ( GEN (w1,the InitS of S)) = ( GEN (w2,the InitS of S))

    proof

      assume

       A1: S is calculating_type;

      let w1, w2;

      assume that

       A2: (w1 . 1) = (w2 . 1) and

       A3: ( len w1) = ( len w2);

      

       A4: ( len ( GEN (w1,the InitS of S))) = (1 + ( len w1)) by FSM_1:def 2;

      ( len ( GEN (w2,the InitS of S))) = (1 + ( len w2)) by FSM_1:def 2;

      hence thesis by A1, A2, A3, A4, Th4, TREES_1: 4;

    end;

     Lm1:

    now

      let I, S, w, q;

      

       A1: ( dom ( GEN (w,q))) = ( Seg ( len ( GEN (w,q)))) by FINSEQ_1:def 3

      .= ( Seg (( len w) + 1)) by FSM_1:def 2;

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

      then

       A2: 1 in ( dom ( GEN (w,q))) by A1, FINSEQ_1: 1;

      (( GEN (w,q)) . 1) = q by FSM_1:def 2;

      then [1, q] in ( GEN (w,q)) by A2, FUNCT_1:def 2;

      then { [1, q]} c= ( GEN (w,q)) by ZFMISC_1: 31;

      then <*q*> c= ( GEN (w,q)) by FINSEQ_1:def 5;

      then ( GEN (( <*> I),q)) c= ( GEN (w,q)) by FSM_1: 1;

      hence (( GEN (( <*> I),q)),( GEN (w,q))) are_c=-comparable ;

    end;

     Lm2:

    now

      let p,q be FinSequence such that

       A1: p <> {} and

       A2: q <> {} and

       A3: (p . ( len p)) = (q . 1);

      consider p1 be FinSequence, x be object such that

       A4: p = (p1 ^ <*x*>) by A1, FINSEQ_1: 46;

      consider y be object, q1 be FinSequence such that

       A5: q = ( <*y*> ^ q1) and ( len q) = (( len q1) + 1) by A2, REWRITE1: 5;

      

       A6: ( len p) = (( len p1) + ( len <*x*>)) by A4, FINSEQ_1: 22

      .= (( len p1) + 1) by FINSEQ_1: 39;

      then

       A7: (p . ( len p)) = x by A4, FINSEQ_1: 42;

      

       A8: (q . 1) = y by A5, FINSEQ_1: 41;

      (( Del (p,( len p))) ^ q) = (p1 ^ ( <*y*> ^ q1)) by A4, A5, A6, WSIERP_1: 40

      .= (p ^ q1) by A3, A4, A7, A8, FINSEQ_1: 32;

      hence (( Del (p,( len p))) ^ q) = (p ^ ( Del (q,1))) by A5, WSIERP_1: 40;

    end;

    theorem :: FSM_2:7

    

     Th7: (for w1, w2 st (w1 . 1) = (w2 . 1) & ( len w1) = ( len w2) holds ( GEN (w1,the InitS of S)) = ( GEN (w2,the InitS of S))) implies S is calculating_type

    proof

      assume

       A1: for w1, w2 st (w1 . 1) = (w2 . 1) & ( len w1) = ( len w2) holds ( GEN (w1,the InitS of S)) = ( GEN (w2,the InitS of S));

      now

        let w1, w2;

        assume

         A2: (w1 . 1) = (w2 . 1);

        thus (( GEN (w1,the InitS of S)),( GEN (w2,the InitS of S))) are_c=-comparable

        proof

          per cases ;

            suppose w1 = ( <*> I) or w2 = ( <*> I);

            hence thesis by Lm1;

          end;

            suppose

             A3: w1 <> {} & w2 <> {} ;

            reconsider v1 = (w2 | ( Seg ( len w1))), v2 = (w1 | ( Seg ( len w2))) as FinSequence of I by FINSEQ_1: 18;

            ( len w1) <= ( len w2) or ( len w2) <= ( len w1);

            then

             A4: v1 = w2 & ( len v2) = ( len w2) & ( len w1) >= ( len w2) or ( len v1) = ( len w1) & v2 = w1 & ( len w1) <= ( len w2) by FINSEQ_1: 17, FINSEQ_2: 20;

            

             A5: ( len w1) >= ( 0 + 1) by A3, NAT_1: 13;

            

             A6: ( len w2) >= ( 0 + 1) by A3, NAT_1: 13;

            

             A7: (v1 . 1) = (w2 . 1) by A4, A5, FINSEQ_6: 128;

            (v2 . 1) = (w1 . 1) by A4, A6, FINSEQ_6: 128;

            then

             A8: ( GEN (v1,the InitS of S)) = ( GEN (w1,the InitS of S)) or ( GEN (v2,the InitS of S)) = ( GEN (w2,the InitS of S)) by A1, A2, A4, A7;

            consider s1 be FinSequence such that

             A9: w2 = (v1 ^ s1) by FINSEQ_1: 80;

            consider s2 be FinSequence such that

             A10: w1 = (v2 ^ s2) by FINSEQ_1: 80;

            reconsider s1, s2 as FinSequence of I by A9, A10, FINSEQ_1: 36;

            v1 <> {}

            proof

              assume

               A11: v1 = {} ;

              

               A12: ( dom v1) = (( dom w2) /\ ( Seg ( len w1))) by RELAT_1: 61

              .= (( Seg ( len w2)) /\ ( Seg ( len w1))) by FINSEQ_1:def 3;

              ( len w2) <= ( len w1) or ( len w1) <= ( len w2);

              then ( dom v1) = ( Seg ( len w2)) or ( dom v1) = ( Seg ( len w1)) by A12, FINSEQ_1: 7;

              then ( len v1) = ( len w2) or ( len v1) = ( len w1) by FINSEQ_1:def 3;

              hence contradiction by A3, A11;

            end;

            then 1 <= ( len v1) by NAT_1: 14;

            then

             A13: ex WI be Element of I, QI,QI1 be State of S st (WI = (v1 . ( len v1))) & (QI = (( GEN (v1,the InitS of S)) . ( len v1))) & (QI1 = (( GEN (v1,the InitS of S)) . (( len v1) + 1))) & ((WI -succ_of QI) = QI1) by FSM_1:def 2;

            v2 <> {}

            proof

              assume v2 = {} ;

              then

               A14: ( len v2) = 0 ;

              

               A15: ( dom v2) = (( dom w1) /\ ( Seg ( len w2))) by RELAT_1: 61

              .= (( Seg ( len w1)) /\ ( Seg ( len w2))) by FINSEQ_1:def 3;

              ( len w2) <= ( len w1) or ( len w1) <= ( len w2);

              then ( dom v2) = ( Seg ( len w2)) or ( dom v2) = ( Seg ( len w1)) by A15, FINSEQ_1: 7;

              hence contradiction by A3, A14, FINSEQ_1:def 3;

            end;

            then 1 <= ( len v2) by NAT_1: 14;

            then ex WI2 be Element of I, QI2,QI12 be State of S st (WI2 = (v2 . ( len v2))) & (QI2 = (( GEN (v2,the InitS of S)) . ( len v2))) & (QI12 = (( GEN (v2,the InitS of S)) . (( len v2) + 1))) & ((WI2 -succ_of QI2) = QI12) by FSM_1:def 2;

            then

            reconsider q1 = (( GEN (v1,the InitS of S)) . (( len v1) + 1)), q2 = (( GEN (v2,the InitS of S)) . (( len v2) + 1)) as State of S by A13;

            

             A16: (( GEN (s1,q1)) . 1) = q1 by FSM_1:def 2;

            

             A17: (( GEN (s2,q2)) . 1) = q2 by FSM_1:def 2;

            

             A18: ( len ( GEN (v1,the InitS of S))) = (( len v1) + 1) by FSM_1:def 2;

            

             A19: ( len ( GEN (v2,the InitS of S))) = (( len v2) + 1) by FSM_1:def 2;

            (the InitS of S,v1) -leads_to q1;

            

            then

             A20: ( GEN (w2,the InitS of S)) = (( Del (( GEN (v1,the InitS of S)),(( len v1) + 1))) ^ ( GEN (s1,q1))) by A9, FSM_1: 8

            .= (( GEN (v1,the InitS of S)) ^ ( Del (( GEN (s1,q1)),1))) by A16, A18, Lm2;

            (the InitS of S,v2) -leads_to q2;

            

            then ( GEN (w1,the InitS of S)) = (( Del (( GEN (v2,the InitS of S)),(( len v2) + 1))) ^ ( GEN (s2,q2))) by A10, FSM_1: 8

            .= (( GEN (v2,the InitS of S)) ^ ( Del (( GEN (s2,q2)),1))) by A17, A19, Lm2;

            then ( GEN (w1,the InitS of S)) c= ( GEN (w2,the InitS of S)) or ( GEN (w2,the InitS of S)) c= ( GEN (w1,the InitS of S)) by A8, A20, TREES_1: 1;

            hence thesis;

          end;

        end;

      end;

      hence thesis by Th5;

    end;

    definition

      let I, S, q, s;

      :: FSM_2:def2

      pred q is_accessible_via s means ex w be FinSequence of I st (the InitS of S,( <*s*> ^ w)) -leads_to q;

    end

    definition

      let I, S, q;

      :: FSM_2:def3

      attr q is accessible means ex w be FinSequence of I st (the InitS of S,w) -leads_to q;

    end

    theorem :: FSM_2:8

    q is_accessible_via s implies q is accessible;

    theorem :: FSM_2:9

    q is accessible & q <> the InitS of S implies ex s st q is_accessible_via s

    proof

      assume that

       A1: q is accessible and

       A2: q <> the InitS of S;

      consider W be FinSequence of I such that

       A3: (the InitS of S,W) -leads_to q by A1;

      W <> {} by FSM_1:def 2, A2, A3;

      then

      consider S be Element of I, w9 be FinSequence of I such that (W . 1) = S and

       A4: W = ( <*S*> ^ w9) by FINSEQ_3: 102;

      take S;

      thus thesis by A3, A4;

    end;

    theorem :: FSM_2:10

    the InitS of S is accessible

    proof

      set w = ( <*> I);

      (( GEN (w,the InitS of S)) . (( len w) + 1)) = the InitS of S by FSM_1:def 2;

      then (the InitS of S,w) -leads_to the InitS of S;

      hence thesis;

    end;

    theorem :: FSM_2:11

    S is calculating_type & q is_accessible_via s implies ex m be non zero Element of NAT st for w st (( len w) + 1) >= m & (w . 1) = s holds q = (( GEN (w,the InitS of S)) . m) & for i st i < m holds (( GEN (w,the InitS of S)) . i) <> q

    proof

      assume

       A1: S is calculating_type;

      given w be FinSequence of I such that

       A2: (the InitS of S,( <*s*> ^ w)) -leads_to q;

      defpred P[ Nat] means q = (( GEN (( <*s*> ^ w),the InitS of S)) . $1) & $1 >= 1 & $1 <= (( len ( <*s*> ^ w)) + 1);

      

       A3: (( len ( <*s*> ^ w)) + 1) >= 1 by NAT_1: 11;

      q = (( GEN (( <*s*> ^ w),the InitS of S)) . (( len ( <*s*> ^ w)) + 1)) by A2;

      then

       A4: ex m be Nat st P[m] by A3;

      consider m be Nat such that

       A5: P[m] and

       A6: for k be Nat st P[k] holds m <= k from NAT_1:sch 5( A4);

      reconsider m as non zero Element of NAT by A5, ORDINAL1:def 12;

      take m;

      let w1 such that

       A7: (( len w1) + 1) >= m and

       A8: (w1 . 1) = s;

      (( <*s*> ^ w) . 1) = s by FINSEQ_1: 41;

      then (( GEN (w1,the InitS of S)),( GEN (( <*s*> ^ w),the InitS of S))) are_c=-comparable by A1, A8, Th4;

      then

       A9: ( GEN (w1,the InitS of S)) c= ( GEN (( <*s*> ^ w),the InitS of S)) or ( GEN (( <*s*> ^ w),the InitS of S)) c= ( GEN (w1,the InitS of S));

      

       A10: ( dom ( GEN (( <*s*> ^ w),the InitS of S))) = ( Seg ( len ( GEN (( <*s*> ^ w),the InitS of S)))) by FINSEQ_1:def 3

      .= ( Seg (( len ( <*s*> ^ w)) + 1)) by FSM_1:def 2;

      

       A11: ( dom ( GEN (w1,the InitS of S))) = ( Seg ( len ( GEN (w1,the InitS of S)))) by FINSEQ_1:def 3

      .= ( Seg (( len w1) + 1)) by FSM_1:def 2;

      

       A12: m in ( dom ( GEN (( <*s*> ^ w),the InitS of S))) by A5, A10, FINSEQ_1: 1;

      m in ( dom ( GEN (w1,the InitS of S))) by A5, A7, A11, FINSEQ_1: 1;

      hence q = (( GEN (w1,the InitS of S)) . m) by A5, A9, A12, GRFUNC_1: 2;

      let i;

      assume

       A13: i < m;

      

       A14: 1 <= i by NAT_1: 14;

      

       A15: i <= (( len ( <*s*> ^ w)) + 1) by A5, A13, XXREAL_0: 2;

      

       A16: i <= (( len w1) + 1) by A7, A13, XXREAL_0: 2;

      

       A17: ( dom ( GEN (w1,the InitS of S))) = ( Seg ( len ( GEN (w1,the InitS of S)))) by FINSEQ_1:def 3

      .= ( Seg (( len w1) + 1)) by FSM_1:def 2;

      ( dom ( GEN (( <*s*> ^ w),the InitS of S))) = ( Seg ( len ( GEN (( <*s*> ^ w),the InitS of S)))) by FINSEQ_1:def 3

      .= ( Seg (( len ( <*s*> ^ w)) + 1)) by FSM_1:def 2;

      then

       A18: i in ( dom ( GEN (( <*s*> ^ w),the InitS of S))) by A14, A15, FINSEQ_1: 1;

      

       A19: i in ( dom ( GEN (w1,the InitS of S))) by A14, A16, A17, FINSEQ_1: 1;

      assume (( GEN (w1,the InitS of S)) . i) = q;

      then q = (( GEN (( <*s*> ^ w),the InitS of S)) . i) by A9, A18, A19, GRFUNC_1: 2;

      hence thesis by A6, A13, A14, A15;

    end;

    definition

      let I, S;

      :: FSM_2:def4

      attr S is regular means for q be State of S holds q is accessible;

    end

    theorem :: FSM_2:12

    (for s1, s2, q holds (the Tran of S . [q, s1]) = (the Tran of S . [q, s2])) implies S is calculating_type

    proof

      assume

       A1: for s1, s2, q holds (the Tran of S . [q, s1]) = (the Tran of S . [q, s2]);

      for j holds for w1, w2 st (w1 . 1) = (w2 . 1) & j <= (( len w1) + 1) & j <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . j) = (( GEN (w2,the InitS of S)) . j)

      proof

        let j;

        let w1, w2;

        assume that

         A2: (w1 . 1) = (w2 . 1) and

         A3: j <= (( len w1) + 1) and

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

        defpred P[ Nat] means for w1, w2 st (w1 . 1) = (w2 . 1) & $1 <= (( len w1) + 1) & $1 <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . $1) = (( GEN (w2,the InitS of S)) . $1);

        

         A5: P[1]

        proof

          let w1, w2;

          (( GEN (w1,the InitS of S)) . 1) = the InitS of S by FSM_1:def 2;

          hence thesis by FSM_1:def 2;

        end;

        

         A6: for h be non zero Nat st P[h] holds P[(h + 1)]

        proof

          let h be non zero Nat;

          assume

           A7: for w1, w2 st (w1 . 1) = (w2 . 1) & h <= (( len w1) + 1) & h <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . h) = (( GEN (w2,the InitS of S)) . h);

          let w1, w2;

          assume that

           A8: (w1 . 1) = (w2 . 1) and

           A9: (h + 1) <= (( len w1) + 1) and

           A10: (h + 1) <= (( len w2) + 1);

          

           A11: h <= ( len w1) by A9, XREAL_1: 6;

          

           A12: h <= (( len w1) + 1) by A9, NAT_1: 13;

          1 <= h by NAT_1: 14;

          then

          consider WI be Element of I, QI,QI1 be State of S such that WI = (w1 . h) and

           A13: QI = (( GEN (w1,the InitS of S)) . h) and

           A14: QI1 = (( GEN (w1,the InitS of S)) . (h + 1)) and

           A15: (WI -succ_of QI) = QI1 by A11, FSM_1:def 2;

          

           A16: h <= ( len w2) by A10, XREAL_1: 6;

          

           A17: h <= (( len w2) + 1) by A10, NAT_1: 13;

          1 <= h by NAT_1: 14;

          then

          consider WI2 be Element of I, QI2,QI12 be State of S such that WI2 = (w2 . h) and

           A18: QI2 = (( GEN (w2,the InitS of S)) . h) and

           A19: QI12 = (( GEN (w2,the InitS of S)) . (h + 1)) and

           A20: (WI2 -succ_of QI2) = QI12 by A16, FSM_1:def 2;

          QI = QI2 by A7, A8, A12, A13, A17, A18;

          hence thesis by A1, A14, A15, A19, A20;

        end;

        for j be non zero Nat holds P[j] from NAT_1:sch 10( A5, A6);

        hence thesis by A2, A3, A4;

      end;

      hence thesis;

    end;

    theorem :: FSM_2:13

    for S st (for s1, s2, q st q <> the InitS of S holds (the Tran of S . [q, s1]) = (the Tran of S . [q, s2])) & for s, q1 holds (the Tran of S . [q1, s]) <> the InitS of S holds S is calculating_type

    proof

      let S;

      assume that

       A1: for s1, s2, q st q <> the InitS of S holds (the Tran of S . [q, s1]) = (the Tran of S . [q, s2]) and

       A2: for s, q1 holds (the Tran of S . [q1, s]) <> the InitS of S;

      

       A3: for j st j >= 2 holds for w1 st j <= (( len w1) + 1) holds (( GEN (w1,the InitS of S)) . j) <> the InitS of S

      proof

        let j;

        assume j >= 2;

        then j <> 1;

        then

         A4: j is non trivial by NAT_2:def 1;

        defpred P[ Nat] means for w1 st $1 <= (( len w1) + 1) holds (( GEN (w1,the InitS of S)) . $1) <> the InitS of S;

        

         A5: P[2]

        proof

          let w1;

          assume 2 <= (( len w1) + 1);

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

          then 1 <= ( len w1) by XREAL_1: 6;

          then ex WI be Element of I, QI,QI1 be State of S st (WI = (w1 . 1)) & (QI = (( GEN (w1,the InitS of S)) . 1)) & (QI1 = (( GEN (w1,the InitS of S)) . (1 + 1))) & ((WI -succ_of QI) = QI1) by FSM_1:def 2;

          hence thesis by A2;

        end;

        

         A6: for h be non trivial Nat st P[h] holds P[(h + 1)]

        proof

          let h be non trivial Nat;

          assume for w1 st h <= (( len w1) + 1) holds (( GEN (w1,the InitS of S)) . h) <> the InitS of S;

          let w1;

          assume

           A7: (h + 1) <= (( len w1) + 1);

          

           A8: 1 <= h by NAT_1: 14;

          h <= ( len w1) by A7, XREAL_1: 6;

          then ex WI be Element of I, QI,QI1 be State of S st (WI = (w1 . h)) & (QI = (( GEN (w1,the InitS of S)) . h)) & (QI1 = (( GEN (w1,the InitS of S)) . (h + 1))) & ((WI -succ_of QI) = QI1) by A8, FSM_1:def 2;

          hence thesis by A2;

        end;

        for h be non trivial Nat holds P[h] from NAT_2:sch 2( A5, A6);

        hence thesis by A4;

      end;

      for j holds for w1, w2 st (w1 . 1) = (w2 . 1) & j <= (( len w1) + 1) & j <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . j) = (( GEN (w2,the InitS of S)) . j)

      proof

        let j;

        let w1, w2;

        assume that

         A9: (w1 . 1) = (w2 . 1) and

         A10: j <= (( len w1) + 1) and

         A11: j <= (( len w2) + 1);

        defpred P[ Nat] means for w1, w2 st (w1 . 1) = (w2 . 1) & $1 <= (( len w1) + 1) & $1 <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . $1) = (( GEN (w2,the InitS of S)) . $1);

        

         A12: P[1]

        proof

          let w1, w2;

          (( GEN (w1,the InitS of S)) . 1) = the InitS of S by FSM_1:def 2;

          hence thesis by FSM_1:def 2;

        end;

        

         A13: for h be non zero Nat st P[h] holds P[(h + 1)]

        proof

          let h be non zero Nat;

          assume

           A14: for w1, w2 st (w1 . 1) = (w2 . 1) & h <= (( len w1) + 1) & h <= (( len w2) + 1) holds (( GEN (w1,the InitS of S)) . h) = (( GEN (w2,the InitS of S)) . h);

          let w1, w2;

          assume that

           A15: (w1 . 1) = (w2 . 1) and

           A16: (h + 1) <= (( len w1) + 1) and

           A17: (h + 1) <= (( len w2) + 1);

          

           A18: h <= ( len w1) by A16, XREAL_1: 6;

          

           A19: h <= (( len w1) + 1) by A16, NAT_1: 13;

          

           A20: 1 <= h by NAT_1: 14;

          then

          consider WI be Element of I, QI,QI1 be State of S such that

           A21: WI = (w1 . h) and

           A22: QI = (( GEN (w1,the InitS of S)) . h) and

           A23: QI1 = (( GEN (w1,the InitS of S)) . (h + 1)) and

           A24: (WI -succ_of QI) = QI1 by A18, FSM_1:def 2;

          

           A25: h <= ( len w2) by A17, XREAL_1: 6;

          

           A26: h <= (( len w2) + 1) by A17, NAT_1: 13;

          1 <= h by NAT_1: 14;

          then

          consider WI2 be Element of I, QI2,QI12 be State of S such that

           A27: WI2 = (w2 . h) and

           A28: QI2 = (( GEN (w2,the InitS of S)) . h) and

           A29: QI12 = (( GEN (w2,the InitS of S)) . (h + 1)) and

           A30: (WI2 -succ_of QI2) = QI12 by A25, FSM_1:def 2;

          

           A31: QI = QI2 by A14, A15, A19, A22, A26, A28;

          

           A32: h in NAT by ORDINAL1:def 12;

          h = 1 or h > 1 by A20, XXREAL_0: 1;

          then h = 1 or h >= (1 + 1) by NAT_1: 13;

          hence thesis by A1, A3, A15, A19, A21, A22, A23, A24, A27, A29, A30, A31, A32;

        end;

        for j be non zero Nat holds P[j] from NAT_1:sch 10( A12, A13);

        hence thesis by A9, A10, A11;

      end;

      hence thesis;

    end;

    theorem :: FSM_2:14

    

     Th14: S is regular & S is calculating_type implies for s1, s2, q st q <> the InitS of S holds (( GEN ( <*s1*>,q)) . 2) = (( GEN ( <*s2*>,q)) . 2)

    proof

      assume that

       A1: S is regular and

       A2: S is calculating_type;

      let s1, s2, q;

      assume

       A3: q <> the InitS of S;

      q is accessible by A1;

      then

      consider w such that

       A4: (the InitS of S,w) -leads_to q;

      w <> {} by FSM_1:def 2, A3, A4;

      then

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

       A5: w = ( <*x*> ^ w9) by FINSEQ_3: 102;

      set w1 = (w ^ <*s1*>), w2 = (w ^ <*s2*>);

      ( len <*x*>) = 1 by FINSEQ_1: 39;

      then (( len <*x*>) + ( len w9)) >= 1 by NAT_1: 11;

      then ( len w) >= 1 by A5, FINSEQ_1: 22;

      then

       A6: 1 in ( dom w) by FINSEQ_3: 25;

      then (w . 1) = (w1 . 1) by FINSEQ_1:def 7;

      then

       A7: (w1 . 1) = (w2 . 1) by A6, FINSEQ_1:def 7;

      

       A8: ( len <*s1*>) = 1 by FINSEQ_1: 39;

      then

       A9: ( len w1) = (( len w) + 1) by FINSEQ_1: 22;

      

       A10: ( len <*s2*>) = 1 by FINSEQ_1: 39;

      then

       A11: ( len w2) = (( len w) + 1) by FINSEQ_1: 22;

      

       A12: ( len w1) = ( len w2) by A9, A10, FINSEQ_1: 22;

      set p = ( Del (( GEN (w,the InitS of S)),(( len w) + 1)));

      set p1 = ( GEN ( <*s1*>,q));

      

       A13: ( GEN (w1,the InitS of S)) = (p ^ p1) by A4, FSM_1: 8;

      

       A14: ( len ( GEN (w,the InitS of S))) = (( len w) + 1) by FSM_1:def 2;

      then

       A15: ( len p) = ( len w) by PRE_POLY: 12;

      

       A16: ( len p1) = (( len <*s1*>) + 1) by FSM_1:def 2

      .= (1 + 1) by FINSEQ_1: 39;

      

       A17: ( len ( GEN (w1,the InitS of S))) = ( len (p ^ p1)) by A4, FSM_1: 8

      .= (( len p) + ( len p1)) by FINSEQ_1: 22

      .= (( len w) + (1 + 1)) by A14, A16, PRE_POLY: 12

      .= ((( len w) + 1) + 1)

      .= (( len w1) + 1) by A8, FINSEQ_1: 22;

      

       A18: (( len p) + 1) <= (( len w1) + 1) by A9, A15, NAT_1: 11;

      ( len (p ^ p1)) = (( len w1) + 1) by A4, A17, FSM_1: 8;

      then (( len p) + ( len p1)) = (( len w1) + 1) by FINSEQ_1: 22;

      

      then

       A19: (( GEN (w1,the InitS of S)) . (( len w1) + 1)) = (p1 . ((( len w1) + 1) - ( len p))) by A13, A18, FINSEQ_1: 23

      .= (p1 . ((( len w1) + 1) - ( len w))) by A14, PRE_POLY: 12

      .= (p1 . (((( len w) + 1) + 1) - ( len w))) by A8, FINSEQ_1: 22

      .= (p1 . 2);

      set p2 = ( GEN ( <*s2*>,q));

      

       A20: ( GEN (w2,the InitS of S)) = (p ^ p2) by A4, FSM_1: 8;

      

       A21: ( len p2) = (( len <*s2*>) + 1) by FSM_1:def 2

      .= (1 + 1) by FINSEQ_1: 39;

      

       A22: ( len ( GEN (w2,the InitS of S))) = ( len (p ^ p2)) by A4, FSM_1: 8

      .= (( len p) + ( len p2)) by FINSEQ_1: 22

      .= (( len w) + (1 + 1)) by A14, A21, PRE_POLY: 12

      .= ((( len w) + 1) + 1)

      .= (( len w2) + 1) by A10, FINSEQ_1: 22;

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

      then

       A23: (( len p) + 1) <= (( len w2) + 1) by A14, PRE_POLY: 12;

      ( len (p ^ p2)) = (( len w2) + 1) by A4, A22, FSM_1: 8;

      then (( len w2) + 1) <= (( len p) + ( len p2)) by FINSEQ_1: 22;

      

      then (( GEN (w2,the InitS of S)) . (( len w2) + 1)) = (p2 . ((( len w2) + 1) - ( len p))) by A20, A23, FINSEQ_1: 23

      .= (p2 . ((( len w2) + 1) - ( len w))) by A14, PRE_POLY: 12

      .= (p2 . (((( len w) + 1) + 1) - ( len w))) by A10, FINSEQ_1: 22

      .= (p2 . 2);

      hence thesis by A2, A7, A12, A19;

    end;

    theorem :: FSM_2:15

    S is regular & S is calculating_type implies for s1, s2, q st q <> the InitS of S holds (the Tran of S . [q, s1]) = (the Tran of S . [q, s2])

    proof

      assume that

       A1: S is regular and

       A2: S is calculating_type;

      let s1, s2, q;

      assume

       A3: q <> the InitS of S;

      set w1 = <*s1*>;

      set w2 = <*s2*>;

      

       A4: ( len w1) = ( 0 + 1) by FINSEQ_1: 39;

      reconsider j = ( len w1) as non zero Element of NAT ;

      consider WI be Element of I, QI,QI1 be State of S such that

       A5: WI = (w1 . j) and

       A6: QI = (( GEN (w1,q)) . j) and

       A7: QI1 = (( GEN (w1,q)) . (j + 1)) and

       A8: (WI -succ_of QI) = QI1 by A4, FSM_1:def 2;

      WI = s1 by A4, A5, FINSEQ_1:def 8;

      then

       A9: QI1 = (s1 -succ_of q) by A4, A6, A8, FSM_1:def 2;

      

       A10: ( len w2) = ( 0 + 1) by FINSEQ_1: 39;

      reconsider h = ( len w2) as non zero Element of NAT ;

      consider WI2 be Element of I, QI2,QI12 be State of S such that

       A11: WI2 = (w2 . h) and

       A12: QI2 = (( GEN (w2,q)) . h) and

       A13: QI12 = (( GEN (w2,q)) . (h + 1)) and

       A14: (WI2 -succ_of QI2) = QI12 by A10, FSM_1:def 2;

      

       A15: QI2 = q by A10, A12, FSM_1:def 2;

      WI2 = s2 by A10, A11, FINSEQ_1:def 8;

      hence thesis by A1, A2, A3, A4, A7, A9, A10, A13, A14, A15, Th14;

    end;

    theorem :: FSM_2:16

    S is regular & S is calculating_type implies for s, s1, s2, q st (the Tran of S . [the InitS of S, s1]) <> (the Tran of S . [the InitS of S, s2]) holds (the Tran of S . [q, s]) <> the InitS of S

    proof

      assume that

       A1: S is regular and

       A2: S is calculating_type;

      let s, s1, s2, q;

      assume

       A3: (the Tran of S . [the InitS of S, s1]) <> (the Tran of S . [the InitS of S, s2]);

      q is accessible by A1;

      then

      consider w such that

       A4: (the InitS of S,w) -leads_to q;

      

       A5: (( GEN (w,the InitS of S)) . (( len w) + 1)) = q by A4;

      assume

       A6: (the Tran of S . [q, s]) = the InitS of S;

      reconsider w1 = <*s, s1*>, w2 = <*s, s2*> as FinSequence of I;

      

       A7: ( GEN (w1,q)) = <*q, the InitS of S, (the Tran of S . [the InitS of S, s1])*> by A6, Th2;

      

       A8: ( GEN (w2,q)) = <*q, the InitS of S, (the Tran of S . [the InitS of S, s2])*> by A6, Th2;

      

       A9: (( GEN (w1,q)) . 3) = (the Tran of S . [the InitS of S, s1]) by A7, FINSEQ_1: 45;

      

       A10: (( GEN (w2,q)) . 3) = (the Tran of S . [the InitS of S, s2]) by A8, FINSEQ_1: 45;

      

       A11: ( len w1) = 2 by FINSEQ_1: 44;

      

       A12: ( len w2) = 2 by FINSEQ_1: 44;

      

       A13: 3 <= (( len w1) + 1) by A11;

      

       A14: 3 <= (( len w2) + 1) by A12;

      

       A15: (( GEN ((w ^ w1),the InitS of S)) . (( len w) + 3)) = (the Tran of S . [the InitS of S, s1]) by A4, A9, A13, FSM_1: 7;

      

       A16: (( GEN ((w ^ w2),the InitS of S)) . (( len w) + 3)) = (the Tran of S . [the InitS of S, s2]) by A4, A10, A14, FSM_1: 7;

      per cases ;

        suppose w = {} ;

        then

         A17: ( len w) = 0 ;

        

         A18: ( GEN (w1,the InitS of S)) = <*the InitS of S, (the Tran of S . [the InitS of S, s]), (the Tran of S . [(the Tran of S . [the InitS of S, s]), s1])*> by Th2;

        

         A19: ( GEN (w2,the InitS of S)) = <*the InitS of S, (the Tran of S . [the InitS of S, s]), (the Tran of S . [(the Tran of S . [the InitS of S, s]), s2])*> by Th2;

        

         A20: (w1 . 1) = s by FINSEQ_1: 44;

        

         A21: (w2 . 1) = s by FINSEQ_1: 44;

        

         A22: 3 <= (( len w1) + 1) by A11;

        

         A23: 3 <= (( len w2) + 1) by A12;

        

         A24: (( GEN (w1,the InitS of S)) . 3) = (the Tran of S . [(the Tran of S . [the InitS of S, s]), s1]) by A18, FINSEQ_1: 45

        .= (the Tran of S . [the InitS of S, s1]) by A5, A6, A17, FSM_1:def 2;

        (( GEN (w2,the InitS of S)) . 3) = (the Tran of S . [(the Tran of S . [the InitS of S, s]), s2]) by A19, FINSEQ_1: 45

        .= (the Tran of S . [the InitS of S, s2]) by A5, A6, A17, FSM_1:def 2;

        hence contradiction by A2, A3, A20, A21, A22, A23, A24;

      end;

        suppose w <> {} ;

        then

        consider s9 be object, w9 be FinSequence such that

         A25: w = ( <*s9*> ^ w9) and ( len w) = (( len w9) + 1) by REWRITE1: 5;

        ( dom <*s9*>) = ( Seg 1) by FINSEQ_1:def 8;

        then

         A26: 1 in ( dom <*s9*>) by FINSEQ_1: 1;

        

        then

         A27: (w . 1) = ( <*s9*> . 1) by A25, FINSEQ_1:def 7

        .= s9 by FINSEQ_1:def 8;

        

         A28: ( dom <*s9*>) c= ( dom w) by A25, FINSEQ_1: 26;

        then

         A29: ((w ^ w1) . 1) = s9 by A26, A27, FINSEQ_1:def 7;

        

         A30: ((w ^ w2) . 1) = s9 by A26, A27, A28, FINSEQ_1:def 7;

        

         A31: (( len (w ^ w1)) + 1) = ((( len w) + 2) + 1) by A11, FINSEQ_1: 22;

        (( len (w ^ w2)) + 1) = ((( len w) + 2) + 1) by A12, FINSEQ_1: 22;

        hence contradiction by A2, A3, A15, A16, A29, A30, A31;

      end;

    end;

    begin

    definition

      let I be set;

      struct ( FSM over I) SM_Final over I (# the carrier -> set,

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

the InitS -> Element of the carrier,

the FinalS -> Subset of the carrier #)

       attr strict strict;

    end

    registration

      let I be set;

      cluster non empty for SM_Final over I;

      existence

      proof

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

        take S = SM_Final (# A, T, I, F #);

        thus the carrier of S is non empty;

      end;

    end

    definition

      let I, s;

      let S be non empty SM_Final over I;

      :: FSM_2:def5

      pred s leads_to_final_state_of S means ex q be State of S st q is_accessible_via s & q in the FinalS of S;

    end

    definition

      let I;

      let S be non empty SM_Final over I;

      :: FSM_2:def6

      attr S is halting means

      : Def6: s leads_to_final_state_of S;

    end

    definition

      let I be set, O be non empty set;

      struct ( SM_Final over I, Moore-FSM over I, O) Moore-SM_Final over I,O (# the carrier -> set,

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

the OFun -> Function of the carrier, O,

the InitS -> Element of the carrier,

the FinalS -> Subset of the carrier #)

       attr strict strict;

    end

    registration

      let I be set, O be non empty set;

      cluster non empty strict for Moore-SM_Final over I, O;

      existence

      proof

        set A = the non empty set, T = the Function of [:A, I:], A, o = the Function of A, O, I = the Element of A, F = the Subset of A;

        take S = Moore-SM_Final (# A, T, o, I, F #);

        thus the carrier of S is non empty;

        thus thesis;

      end;

    end

    definition

      let I, O;

      let i,f be set;

      let o be Function of {i, f}, O;

      :: FSM_2:def7

      func I -TwoStatesMooreSM (i,f,o) -> non empty strict Moore-SM_Final over I, O means

      : Def7: the carrier of it = {i, f} & the Tran of it = ( [: {i, f}, I:] --> f) & the OFun of it = o & the InitS of it = i & the FinalS of it = {f};

      uniqueness ;

      existence

      proof

        set X = {i, f};

        reconsider ii = i, ff = f as Element of X by TARSKI:def 2;

        reconsider oo = o as Function of X, O;

         Moore-SM_Final (# X, ( [:X, I:] --> ff), oo, ii, {ff} #) is non empty;

        hence thesis;

      end;

    end

    theorem :: FSM_2:17

    

     Th17: for i,f be set, o be Function of {i, f}, O holds for j st 1 < j & j <= (( len w) + 1) holds (( GEN (w,the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j) = f

    proof

      let i,f be set, o be Function of {i, f}, O;

      let j;

      assume

       A1: 1 < j;

      set M = (I -TwoStatesMooreSM (i,f,o));

      

       A2: the carrier of M = {i, f} by Def7;

      

       A3: the Tran of M = ( [: {i, f}, I:] --> f) by Def7;

      defpred P[ Nat] means $1 <= (( len w) + 1) implies (( GEN (w,the InitS of (I -TwoStatesMooreSM (i,f,o)))) . $1) = f;

      

       A4: P[2]

      proof

        assume 2 <= (( len w) + 1);

        then (1 + 1) <= (( len w) + 1);

        then 1 < (( len w) + 1) by NAT_1: 13;

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

        then ex WI be Element of I, QI,QI1 be State of M st (WI = (w . 1)) & (QI = (( GEN (w,the InitS of M)) . 1)) & (QI1 = (( GEN (w,the InitS of M)) . (1 + 1))) & ((WI -succ_of QI) = QI1) by FSM_1:def 2;

        hence thesis by A2, A3, FUNCOP_1: 7;

      end;

      

       A5: for k be non trivial Nat st P[k] holds P[(k + 1)]

      proof

        let k be non trivial Nat;

        assume that k <= (( len w) + 1) implies (( GEN (w,the InitS of M)) . k) = f and

         A6: (k + 1) <= (( len w) + 1);

        

         A7: 1 <= k by NAT_2: 19;

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

        then ex WI be Element of I, QI,QI1 be State of M st (WI = (w . k)) & (QI = (( GEN (w,the InitS of M)) . k)) & (QI1 = (( GEN (w,the InitS of M)) . (k + 1))) & ((WI -succ_of QI) = QI1) by A7, FSM_1:def 2;

        hence thesis by A2, A3, FUNCOP_1: 7;

      end;

      

       A8: j is non trivial Nat by A1, NAT_2:def 1;

      for k be non trivial Nat holds P[k] from NAT_2:sch 2( A4, A5);

      hence thesis by A8;

    end;

    registration

      let I, O;

      let i,f be set;

      let o be Function of {i, f}, O;

      cluster (I -TwoStatesMooreSM (i,f,o)) -> calculating_type;

      coherence

      proof

        set M = (I -TwoStatesMooreSM (i,f,o));

        for w1, w2 st (w1 . 1) = (w2 . 1) & ( len w1) = ( len w2) holds ( GEN (w1,the InitS of M)) = ( GEN (w2,the InitS of M))

        proof

          let w1, w2;

          assume that (w1 . 1) = (w2 . 1) and

           A1: ( len w1) = ( len w2);

          reconsider p = ( GEN (w1,the InitS of M)), q = ( GEN (w2,the InitS of M)) as FinSequence;

          

           A2: (p . 1) = the InitS of M by FSM_1:def 2

          .= (q . 1) by FSM_1:def 2;

          

           A3: ( len p) = (( len w1) + 1) by FSM_1:def 2;

          

           A4: ( len q) = (( len w1) + 1) by A1, FSM_1:def 2;

          now

            let j be Nat;

            assume

             A5: 1 <= j;

            

             A6: j in NAT by ORDINAL1:def 12;

            j = 1 or j > 1 by A5, XXREAL_0: 1;

            then (p . j) = (q . j) or (j <= ( len p) implies (p . j) = f & (q . j) = f) by A1, A2, A3, A6, Th17;

            hence j <= ( len p) implies (p . j) = (q . j);

          end;

          hence thesis by A3, A4, FINSEQ_1: 14;

        end;

        hence thesis by Th7;

      end;

    end

    registration

      let I, O;

      let i,f be set;

      let o be Function of {i, f}, O;

      cluster (I -TwoStatesMooreSM (i,f,o)) -> halting;

      coherence

      proof

        let s;

         {i, f} = the carrier of (I -TwoStatesMooreSM (i,f,o)) by Def7;

        then

        reconsider q = f as State of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def 2;

        take q;

        thus q is_accessible_via s

        proof

          take w = ( <*> I);

          ( <*s*> ^ w) = <*s*> by FINSEQ_1: 34;

          then ( len ( <*s*> ^ w)) = 1 by FINSEQ_1: 39;

          hence (( GEN (( <*s*> ^ w),the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (( len ( <*s*> ^ w)) + 1)) = q by Th17;

        end;

        the FinalS of (I -TwoStatesMooreSM (i,f,o)) = {f} by Def7;

        hence thesis by TARSKI:def 1;

      end;

    end

    reserve n,m,o,p for non zero Element of NAT ,

M for non empty Moore-SM_Final over I, O,

q for State of M;

    theorem :: FSM_2:18

    

     Th18: M is calculating_type & s leads_to_final_state_of M implies ex m be non zero Element of NAT st (for w st (( len w) + 1) >= m & (w . 1) = s holds (( GEN (w,the InitS of M)) . m) in the FinalS of M) & for w, j st j <= (( len w) + 1) & (w . 1) = s & j < m holds not (( GEN (w,the InitS of M)) . j) in the FinalS of M

    proof

      assume

       A1: M is calculating_type;

      given q such that

       A2: q is_accessible_via s and

       A3: q in the FinalS of M;

      consider w such that

       A4: (the InitS of M,( <*s*> ^ w)) -leads_to q by A2;

      defpred P[ Nat] means (( GEN (( <*s*> ^ w),the InitS of M)) . $1) in the FinalS of M & $1 >= 1 & $1 <= (( len ( <*s*> ^ w)) + 1);

      

       A5: (( len ( <*s*> ^ w)) + 1) >= 1 by NAT_1: 11;

      q = (( GEN (( <*s*> ^ w),the InitS of M)) . (( len ( <*s*> ^ w)) + 1)) by A4;

      then

       A6: ex m be Nat st P[m] by A3, A5;

      consider m be Nat such that

       A7: P[m] and

       A8: for k be Nat st P[k] holds m <= k from NAT_1:sch 5( A6);

      reconsider m as non zero Element of NAT by A7, ORDINAL1:def 12;

      take m;

      hereby

        let w1 such that

         A9: (( len w1) + 1) >= m and

         A10: (w1 . 1) = s;

        (( <*s*> ^ w) . 1) = s by FINSEQ_1: 41;

        then (( GEN (w1,the InitS of M)),( GEN (( <*s*> ^ w),the InitS of M))) are_c=-comparable by A1, A10, Th4;

        then

         A11: ( GEN (w1,the InitS of M)) c= ( GEN (( <*s*> ^ w),the InitS of M)) or ( GEN (( <*s*> ^ w),the InitS of M)) c= ( GEN (w1,the InitS of M));

        

         A12: ( dom ( GEN (( <*s*> ^ w),the InitS of M))) = ( Seg ( len ( GEN (( <*s*> ^ w),the InitS of M)))) by FINSEQ_1:def 3

        .= ( Seg (( len ( <*s*> ^ w)) + 1)) by FSM_1:def 2;

        

         A13: ( dom ( GEN (w1,the InitS of M))) = ( Seg ( len ( GEN (w1,the InitS of M)))) by FINSEQ_1:def 3

        .= ( Seg (( len w1) + 1)) by FSM_1:def 2;

        

         A14: m in ( dom ( GEN (( <*s*> ^ w),the InitS of M))) by A7, A12, FINSEQ_1: 1;

        m in ( dom ( GEN (w1,the InitS of M))) by A7, A9, A13, FINSEQ_1: 1;

        hence (( GEN (w1,the InitS of M)) . m) in the FinalS of M by A7, A11, A14, GRFUNC_1: 2;

      end;

      let w1;

      let i;

      assume that

       A15: i <= (( len w1) + 1) and

       A16: (w1 . 1) = s and

       A17: i < m;

      (( <*s*> ^ w) . 1) = s by FINSEQ_1: 41;

      then (( GEN (w1,the InitS of M)),( GEN (( <*s*> ^ w),the InitS of M))) are_c=-comparable by A1, A16, Th4;

      then

       A18: ( GEN (w1,the InitS of M)) c= ( GEN (( <*s*> ^ w),the InitS of M)) or ( GEN (( <*s*> ^ w),the InitS of M)) c= ( GEN (w1,the InitS of M));

      

       A19: 1 <= i by NAT_1: 14;

      

       A20: i <= (( len ( <*s*> ^ w)) + 1) by A7, A17, XXREAL_0: 2;

      

       A21: ( dom ( GEN (w1,the InitS of M))) = ( Seg ( len ( GEN (w1,the InitS of M)))) by FINSEQ_1:def 3

      .= ( Seg (( len w1) + 1)) by FSM_1:def 2;

      ( dom ( GEN (( <*s*> ^ w),the InitS of M))) = ( Seg ( len ( GEN (( <*s*> ^ w),the InitS of M)))) by FINSEQ_1:def 3

      .= ( Seg (( len ( <*s*> ^ w)) + 1)) by FSM_1:def 2;

      then

       A22: i in ( dom ( GEN (( <*s*> ^ w),the InitS of M))) by A19, A20, FINSEQ_1: 1;

      

       A23: i in ( dom ( GEN (w1,the InitS of M))) by A15, A19, A21, FINSEQ_1: 1;

      assume (( GEN (w1,the InitS of M)) . i) in the FinalS of M;

      then (( GEN (( <*s*> ^ w),the InitS of M)) . i) in the FinalS of M by A18, A22, A23, GRFUNC_1: 2;

      hence thesis by A8, A17, A19, A20;

    end;

    begin

    definition

      let I, O, M, s;

      let t be object;

      :: FSM_2:def8

      pred t is_result_of s,M means ex m st for w st (w . 1) = s holds (m <= (( len w) + 1) implies t = (the OFun of M . (( GEN (w,the InitS of M)) . m)) & (( GEN (w,the InitS of M)) . m) in the FinalS of M) & for n st n < m & n <= (( len w) + 1) holds not (( GEN (w,the InitS of M)) . n) in the FinalS of M;

    end

    theorem :: FSM_2:19

    the InitS of M in the FinalS of M implies (the OFun of M . the InitS of M) is_result_of (s,M)

    proof

      assume

       A1: the InitS of M in the FinalS of M;

      take 1;

      let w;

      assume (w . 1) = s;

      thus thesis by A1, FSM_1:def 2, NAT_1: 14;

    end;

    theorem :: FSM_2:20

    

     Th20: M is calculating_type & s leads_to_final_state_of M implies ex t st t is_result_of (s,M)

    proof

      assume that

       A1: M is calculating_type and

       A2: s leads_to_final_state_of M;

      consider q such that

       A3: q is_accessible_via s and

       A4: q in the FinalS of M by A2;

      consider w such that

       A5: (the InitS of M,( <*s*> ^ w)) -leads_to q by A3;

      

       A6: (( GEN (( <*s*> ^ w),the InitS of M)) . (( len ( <*s*> ^ w)) + 1)) = q by A5;

      consider m be non zero Element of NAT such that

       A7: for w st (( len w) + 1) >= m & (w . 1) = s holds (( GEN (w,the InitS of M)) . m) in the FinalS of M and

       A8: for w, j st j <= (( len w) + 1) & (w . 1) = s & j < m holds not (( GEN (w,the InitS of M)) . j) in the FinalS of M by A1, A2, Th18;

      

       A9: (( <*s*> ^ w) . 1) = s by FINSEQ_1: 41;

      then

       A10: (( len ( <*s*> ^ w)) + 1) >= m by A4, A6, A8;

      then (( GEN (( <*s*> ^ w),the InitS of M)) . m) in the FinalS of M by A7, A9;

      then

      reconsider t = (the OFun of M . (( GEN (( <*s*> ^ w),the InitS of M)) . m)) as Element of O by FUNCT_2: 5;

      take t, m;

      let w1 such that

       A11: (w1 . 1) = s;

      (( <*s*> ^ w) . 1) = s by FINSEQ_1: 41;

      hence m <= (( len w1) + 1) implies t = (the OFun of M . (( GEN (w1,the InitS of M)) . m)) & (( GEN (w1,the InitS of M)) . m) in the FinalS of M by A1, A7, A10, A11;

      thus thesis by A8, A11;

    end;

    theorem :: FSM_2:21

    

     Th21: s leads_to_final_state_of M implies for t1,t2 be Element of O st t1 is_result_of (s,M) & t2 is_result_of (s,M) holds t1 = t2

    proof

      assume that

       A1: s leads_to_final_state_of M;

      let t1,t2 be Element of O;

      given m such that

       A2: for w1 st (w1 . 1) = s holds (m <= (( len w1) + 1) implies t1 = (the OFun of M . (( GEN (w1,the InitS of M)) . m)) & (( GEN (w1,the InitS of M)) . m) in the FinalS of M) & for n st n < m & n <= (( len w1) + 1) holds not (( GEN (w1,the InitS of M)) . n) in the FinalS of M;

      given o such that

       A3: for w2 st (w2 . 1) = s holds (o <= (( len w2) + 1) implies t2 = (the OFun of M . (( GEN (w2,the InitS of M)) . o)) & (( GEN (w2,the InitS of M)) . o) in the FinalS of M) & for p st p < o & p <= (( len w2) + 1) holds not (( GEN (w2,the InitS of M)) . p) in the FinalS of M;

      consider q be State of M such that

       A4: q is_accessible_via s and

       A5: q in the FinalS of M by A1;

      consider w be FinSequence of I such that

       A6: (the InitS of M,( <*s*> ^ w)) -leads_to q by A4;

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

      

       A7: (( GEN (w1,the InitS of M)) . (( len w1) + 1)) = q by A6;

      

       A8: (( <*s*> ^ w) . 1) = s by FINSEQ_1: 41;

      then

       A9: (( len ( <*s*> ^ w)) + 1) >= m by A2, A5, A7;

      

       A10: o <= (( len w1) + 1) by A3, A5, A7, A8;

      

       A11: o < m or o = m or o > m by XXREAL_0: 1;

      

       A12: (w1 . 1) = s by FINSEQ_1: 41;

      then

       A13: t1 = (the OFun of M . (( GEN (w1,the InitS of M)) . m)) by A2, A9;

      

       A14: (( GEN (w1,the InitS of M)) . m) in the FinalS of M by A2, A9, A12;

      (( GEN (w1,the InitS of M)) . o) in the FinalS of M by A3, A10, A12;

      hence thesis by A2, A3, A9, A10, A11, A12, A13, A14;

    end;

    theorem :: FSM_2:22

    

     Th22: for X be non empty set holds for f be BinOp of X holds for M be non empty Moore-SM_Final over [:X, X:], ( succ X) st M is calculating_type & the carrier of M = ( succ X) & the FinalS of M = X & the InitS of M = X & the OFun of M = ( id the carrier of M) & for x,y be Element of X holds (the Tran of M . [the InitS of M, [x, y]]) = (f . (x,y)) holds M is halting & for x,y be Element of X holds (f . (x,y)) is_result_of ( [x, y],M)

    proof

      let X be non empty set, f be BinOp of X;

      let M be non empty Moore-SM_Final over [:X, X:], ( succ X);

      assume that

       A1: M is calculating_type and

       A2: the carrier of M = ( succ X) and

       A3: the FinalS of M = X and

       A4: the InitS of M = X and

       A5: the OFun of M = ( id the carrier of M) and

       A6: for x,y be Element of X holds (the Tran of M . [the InitS of M, [x, y]]) = (f . (x,y));

      

       A7: not the InitS of M in the FinalS of M by A3, A4;

      now

        let s be Element of [:X, X:];

        consider x,y be object such that

         A9: x in X and

         A10: y in X and

         A11: s = [x, y] by ZFMISC_1:def 2;

        reconsider x, y as Element of X by A9, A10;

        thus s leads_to_final_state_of M

        proof

          reconsider q = (f . (x,y)) as State of M by A2, XBOOLE_0:def 3;

          take q;

          thus q is_accessible_via s

          proof

            take w = ( <*> [:X, X:]);

            reconsider W = ( <*s*> ^ w) as FinSequence of [:X, X:];

            

             A12: W = <* [x, y]*> by A11, FINSEQ_1: 34;

            then ( len W) = 1 by FINSEQ_1: 39;

            then

             A13: ex WI be Element of [:X, X:], QI,QI1 be State of M st (WI = (W . 1)) & (QI = (( GEN (W,the InitS of M)) . 1)) & (QI1 = (( GEN (W,the InitS of M)) . (1 + 1))) & ((WI -succ_of QI) = QI1) by FSM_1:def 2;

            (( GEN (W,the InitS of M)) . (( len W) + 1)) = (( GEN (W,the InitS of M)) . (1 + 1)) by A12, FINSEQ_1: 39

            .= (the Tran of M . [the InitS of M, (W . 1)]) by A13, FSM_1:def 2

            .= (the Tran of M . [the InitS of M, [x, y]]) by A11, FINSEQ_1: 41

            .= (f . (x,y)) by A6;

            hence thesis;

          end;

          thus thesis by A3;

        end;

      end;

      let x,y be Element of X;

      consider m be non zero Element of NAT such that

       A14: for w be FinSequence of [:X, X:] st (( len w) + 1) >= m & (w . 1) = [x, y] holds (( GEN (w,the InitS of M)) . m) in the FinalS of M and

       A15: for w be FinSequence of [:X, X:], i be non zero Element of NAT st i <= (( len w) + 1) & (w . 1) = [x, y] & i < m holds not (( GEN (w,the InitS of M)) . i) in the FinalS of M by A1, A8, Th18;

      take m;

      set s = [x, y], t = (f . (x,y));

      let w be FinSequence of [:X, X:] such that

       A16: (w . 1) = s;

      hereby

        assume

         A17: m <= (( len w) + 1);

        (( GEN (w,the InitS of M)) . 1) = X by A4, FSM_1:def 2;

        then

         A18: m <> 1 by A4, A7, A14, A16, A17;

        m >= 1 by NAT_1: 14;

        then m > 1 by A18, XXREAL_0: 1;

        then

         A19: m >= (1 + 1) by NAT_1: 13;

        then

         A20: (1 + 1) <= (( len w) + 1) by A17, XXREAL_0: 2;

        then 1 <= ( len w) by XREAL_1: 6;

        then ex WI be Element of [:X, X:], QI,QI1 be State of M st (WI = (w . 1)) & (QI = (( GEN (w,the InitS of M)) . 1)) & (QI1 = (( GEN (w,the InitS of M)) . (1 + 1))) & ((WI -succ_of QI) = QI1) by FSM_1:def 2;

        

        then

         A21: (( GEN (w,the InitS of M)) . 2) = (the Tran of M . [the InitS of M, (w . 1)]) by FSM_1:def 2

        .= (f . (x,y)) by A6, A16;

        

         A22: m = 2 or m > 2 by A19, XXREAL_0: 1;

        (f . (x,y)) in ( succ X) by XBOOLE_0:def 3;

        hence t = (the OFun of M . (( GEN (w,the InitS of M)) . m)) by A2, A3, A5, A15, A16, A20, A21, A22, FUNCT_1: 18;

        thus (( GEN (w,the InitS of M)) . m) in the FinalS of M by A14, A16, A17;

      end;

      thus thesis by A15, A16;

    end;

    theorem :: FSM_2:23

    

     Th23: for M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st M is calculating_type & the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = x) & (for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = y) holds for x,y be Element of REAL holds ( max (x,y)) is_result_of ( [x, y],M)

    proof

      deffunc F( Real, Real) = ( In (( max ($1,$2)), REAL ));

      consider f be BinOp of REAL such that

       A1: for x,y be Element of REAL holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

      

       A2: for x,y be Element of REAL holds (f . (x,y)) = ( max (x,y))

      proof

        let x,y be Element of REAL ;

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      let M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A3: M is calculating_type and

       A4: the carrier of M = ( succ REAL ) and

       A5: the FinalS of M = REAL and

       A6: the InitS of M = REAL and

       A7: the OFun of M = ( id the carrier of M);

      assume that

       A8: for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = x and

       A9: for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = y;

      let x,y be Element of REAL ;

      reconsider x, y as Element of REAL ;

      now

        let x,y be Element of REAL ;

        

         A10: x >= y implies (the Tran of M . [the InitS of M, [x, y]]) = x by A8;

        x < y implies (the Tran of M . [the InitS of M, [x, y]]) = y by A9;

        then (the Tran of M . [the InitS of M, [x, y]]) = ( max (x,y)) by A10, XXREAL_0:def 10;

        hence (the Tran of M . [the InitS of M, [x, y]]) = (f . (x,y)) by A2;

      end;

      then (f . (x,y)) is_result_of ( [x, y],M) by A3, A4, A5, A6, A7, Th22;

      hence thesis by A2;

    end;

    theorem :: FSM_2:24

    

     Th24: for M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st M is calculating_type & the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = x) & (for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = y) holds for x,y be Element of REAL holds ( min (x,y)) is_result_of ( [x, y],M)

    proof

      deffunc F( Real, Real) = ( In (( min ($1,$2)), REAL ));

      consider f be BinOp of REAL such that

       A1: for x,y be Element of REAL holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

      

       A2: for x,y be Element of REAL holds (f . (x,y)) = ( min (x,y))

      proof

        let x,y be Element of REAL ;

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      let M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A3: M is calculating_type and

       A4: the carrier of M = ( succ REAL ) and

       A5: the FinalS of M = REAL and

       A6: the InitS of M = REAL and

       A7: the OFun of M = ( id the carrier of M);

      assume that

       A8: for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = x and

       A9: for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = y;

      let x,y be Element of REAL ;

      now

        let x,y be Element of REAL ;

        

         A10: x < y implies (the Tran of M . [the InitS of M, [x, y]]) = x by A8;

        x >= y implies (the Tran of M . [the InitS of M, [x, y]]) = y by A9;

        then (the Tran of M . [the InitS of M, [x, y]]) = ( min (x,y)) by A10, XXREAL_0:def 9;

        hence (the Tran of M . [the InitS of M, [x, y]]) = (f . (x,y)) by A2;

      end;

      then (f . (x,y)) is_result_of ( [x, y],M) by A3, A4, A5, A6, A7, Th22;

      hence thesis by A2;

    end;

    theorem :: FSM_2:25

    

     Th25: for M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st M is calculating_type & the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y holds (the Tran of M . [the InitS of M, [x, y]]) = (x + y)) holds for x,y be Element of REAL holds (x + y) is_result_of ( [x, y],M)

    proof

      deffunc F( Real, Real) = ( In (($1 + $2), REAL ));

      consider f be BinOp of REAL such that

       A1: for x,y be Element of REAL holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

      

       A2: for x,y be Element of REAL holds (f . (x,y)) = (x + y)

      proof

        let x,y be Element of REAL ;

        reconsider x, y as Real;

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      let M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A3: M is calculating_type and

       A4: the carrier of M = ( succ REAL ) and

       A5: the FinalS of M = REAL and

       A6: the InitS of M = REAL and

       A7: the OFun of M = ( id the carrier of M);

      assume

       A8: for x, y holds (the Tran of M . [the InitS of M, [x, y]]) = (x + y);

      let x,y be Element of REAL ;

      now

        let x,y be Element of REAL ;

        (the Tran of M . [the InitS of M, [x, y]]) = (x + y) by A8;

        hence (the Tran of M . [the InitS of M, [x, y]]) = (f . (x,y)) by A2;

      end;

      then (f . (x,y)) is_result_of ( [x, y],M) by A3, A4, A5, A6, A7, Th22;

      hence thesis by A2;

    end;

    theorem :: FSM_2:26

    

     Th26: for M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st M is calculating_type & the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y st x > 0 or y > 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 1) & (for x, y st (x = 0 or y = 0 ) & x <= 0 & y <= 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 0 ) & (for x, y st x < 0 & y < 0 holds (the Tran of M . [the InitS of M, [x, y]]) = ( - 1)) holds for x,y be Element of REAL holds ( max (( sgn x),( sgn y))) is_result_of ( [x, y],M)

    proof

      deffunc F( Real, Real) = ( In (( max (( sgn $1),( sgn $2))), REAL ));

      consider f be BinOp of REAL such that

       A1: for x,y be Element of REAL holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

      

       A2: for x,y be Element of REAL holds (f . (x,y)) = ( max (( sgn x),( sgn y)))

      proof

        let x,y be Element of REAL ;

        reconsider x, y as Real;

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      let M be non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A3: M is calculating_type and

       A4: the carrier of M = ( succ REAL ) and

       A5: the FinalS of M = REAL and

       A6: the InitS of M = REAL and

       A7: the OFun of M = ( id the carrier of M);

      assume that

       A8: for x, y st x > 0 or y > 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 1 and

       A9: for x, y st (x = 0 or y = 0 ) & x <= 0 & y <= 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 0 and

       A10: for x, y st x < 0 & y < 0 holds (the Tran of M . [the InitS of M, [x, y]]) = ( - 1);

      let x,y be Element of REAL ;

      now

        let x,y be Element of REAL ;

        (the Tran of M . [the InitS of M, [x, y]]) = F(x,y)

        proof

          now

            per cases ;

              suppose

               A11: x > 0 ;

              then

               A12: ( sgn x) = 1 by ABSVALUE:def 2;

              now

                per cases ;

                  suppose y > 0 ;

                  then ( sgn y) = 1 by ABSVALUE:def 2;

                  hence thesis by A8, A11, A12;

                end;

                  suppose y = 0 ;

                  then ( sgn y) = 0 by ABSVALUE:def 2;

                  then ( max (( sgn x),( sgn y))) = 1 by A12, XXREAL_0:def 10;

                  hence thesis by A8, A11;

                end;

                  suppose y < 0 ;

                  then ( sgn y) = ( - 1) by ABSVALUE:def 2;

                  then ( max (( sgn x),( sgn y))) = 1 by A12, XXREAL_0:def 10;

                  hence thesis by A8, A11;

                end;

              end;

              hence thesis;

            end;

              suppose

               A13: x = 0 ;

              then

               A14: ( sgn x) = 0 by ABSVALUE:def 2;

              now

                per cases ;

                  suppose

                   A15: y > 0 ;

                  then ( sgn y) = 1 by ABSVALUE:def 2;

                  then ( max (( sgn x),( sgn y))) = 1 by A14, XXREAL_0:def 10;

                  hence thesis by A8, A15;

                end;

                  suppose

                   A16: y = 0 ;

                  then ( sgn y) = 0 by ABSVALUE:def 2;

                  hence thesis by A9, A13, A16;

                end;

                  suppose

                   A17: y < 0 ;

                  then ( sgn y) = ( - 1) by ABSVALUE:def 2;

                  then ( max (( sgn x),( sgn y))) = 0 by A14, XXREAL_0:def 10;

                  hence thesis by A9, A13, A17;

                end;

              end;

              hence thesis;

            end;

              suppose

               A18: x < 0 ;

              then

               A19: ( sgn x) = ( - 1) by ABSVALUE:def 2;

              now

                per cases ;

                  suppose

                   A20: y > 0 ;

                  then ( sgn y) = 1 by ABSVALUE:def 2;

                  then ( max (( sgn x),( sgn y))) = 1 by A19, XXREAL_0:def 10;

                  hence thesis by A8, A20;

                end;

                  suppose

                   A21: y = 0 ;

                  then ( sgn y) = 0 by ABSVALUE:def 2;

                  then ( max (( sgn x),( sgn y))) = 0 by A19, XXREAL_0:def 10;

                  hence thesis by A9, A18, A21;

                end;

                  suppose

                   A22: y < 0 ;

                  then ( sgn y) = ( - 1) by ABSVALUE:def 2;

                  hence thesis by A10, A18, A19, A22;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence (the Tran of M . [the InitS of M, [x, y]]) = (f . (x,y)) by A2;

      end;

      then (f . (x,y)) is_result_of ( [x, y],M) by A3, A4, A5, A6, A7, Th22;

      hence thesis by A2;

    end;

    registration

      let I, O;

      cluster calculating_type halting for non empty Moore-SM_Final over I, O;

      existence

      proof

        set f = the Function of { 0 , 1}, O;

        take (I -TwoStatesMooreSM ( 0 ,1,f));

        thus thesis;

      end;

    end

    registration

      let I;

      cluster calculating_type halting for non empty SM_Final over I;

      existence

      proof

        set O = the non empty set;

        set M = the calculating_type halting non empty Moore-SM_Final over I, O;

        take M;

        thus thesis;

      end;

    end

    definition

      let I, O;

      let M be calculating_type halting non empty Moore-SM_Final over I, O;

      let s;

      

       A1: s leads_to_final_state_of M by Def6;

      :: FSM_2:def9

      func Result (s,M) -> Element of O means

      : Def9: it is_result_of (s,M);

      uniqueness by A1, Th21;

      existence by A1, Th20;

    end

    theorem :: FSM_2:27

    for f be Function of { 0 , 1}, O holds ( Result (s,(I -TwoStatesMooreSM ( 0 ,1,f)))) = (f . 1)

    proof

      let f be Function of { 0 , 1}, O;

      set M = (I -TwoStatesMooreSM ( 0 ,1,f));

      reconsider 01 = 1 as Element of { 0 , 1} by TARSKI:def 2;

      

       A1: s leads_to_final_state_of M by Def6;

      

       A2: the FinalS of M = {1} by Def7;

      

       A3: the OFun of M = f by Def7;

      consider m be non zero Element of NAT such that

       A4: for w st (( len w) + 1) >= m & (w . 1) = s holds (( GEN (w,the InitS of M)) . m) in the FinalS of M and

       A5: for w, j st j <= (( len w) + 1) & (w . 1) = s & j < m holds not (( GEN (w,the InitS of M)) . j) in the FinalS of M by A1, Th18;

      now

        take m;

        let w;

        assume

         A6: (w . 1) = s;

        hereby

          assume m <= (( len w) + 1);

          then (( GEN (w,the InitS of M)) . m) in the FinalS of M by A4, A6;

          hence (f . 1) = (the OFun of M . (( GEN (w,the InitS of M)) . m)) & (( GEN (w,the InitS of M)) . m) in the FinalS of M by A2, A3, TARSKI:def 1;

        end;

        thus for n st n < m & n <= (( len w) + 1) holds not (( GEN (w,the InitS of M)) . n) in the FinalS of M by A5, A6;

      end;

      then (f . 01) is_result_of (s,M);

      hence thesis by Def9;

    end;

    theorem :: FSM_2:28

    for M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = x) & (for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = y) holds for x,y be Element of REAL holds ( Result ( [x, y],M)) = ( max (x,y))

    proof

      let M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A1: the carrier of M = ( succ REAL ) and

       A2: the FinalS of M = REAL and

       A3: the InitS of M = REAL and

       A4: the OFun of M = ( id the carrier of M) and

       A5: for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = x and

       A6: for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = y;

      let x,y be Element of REAL ;

      ( max (x,y)) in REAL by XREAL_0:def 1;

      then

       A7: ( max (x,y)) in ( succ REAL ) by XBOOLE_0:def 3;

      ( max (x,y)) is_result_of ( [x, y],M) by A1, A2, A3, A4, A5, A6, Th23;

      hence thesis by A7, Def9;

    end;

    theorem :: FSM_2:29

    for M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = x) & (for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = y) holds for x,y be Element of REAL holds ( Result ( [x, y],M)) = ( min (x,y))

    proof

      let M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A1: the carrier of M = ( succ REAL ) and

       A2: the FinalS of M = REAL and

       A3: the InitS of M = REAL and

       A4: the OFun of M = ( id the carrier of M) and

       A5: for x, y st x < y holds (the Tran of M . [the InitS of M, [x, y]]) = x and

       A6: for x, y st x >= y holds (the Tran of M . [the InitS of M, [x, y]]) = y;

      let x,y be Element of REAL ;

      ( min (x,y)) in REAL by XREAL_0:def 1;

      then

       A7: ( min (x,y)) in ( succ REAL ) by XBOOLE_0:def 3;

      ( min (x,y)) is_result_of ( [x, y],M) by A1, A2, A3, A4, A5, A6, Th24;

      hence thesis by A7, Def9;

    end;

    theorem :: FSM_2:30

    for M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y holds (the Tran of M . [the InitS of M, [x, y]]) = (x + y)) holds for x,y be Element of REAL holds ( Result ( [x, y],M)) = (x + y)

    proof

      let M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A1: the carrier of M = ( succ REAL ) and

       A2: the FinalS of M = REAL and

       A3: the InitS of M = REAL and

       A4: the OFun of M = ( id the carrier of M) and

       A5: for x, y holds (the Tran of M . [the InitS of M, [x, y]]) = (x + y);

      let x,y be Element of REAL ;

      

       A6: (x + y) in ( succ REAL ) by XBOOLE_0:def 3;

      (x + y) is_result_of ( [x, y],M) by A1, A2, A3, A4, A5, Th25;

      hence thesis by A6, Def9;

    end;

    theorem :: FSM_2:31

    for M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL ) st the carrier of M = ( succ REAL ) & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = ( id the carrier of M) & (for x, y st x > 0 or y > 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 1) & (for x, y st (x = 0 or y = 0 ) & x <= 0 & y <= 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 0 ) & (for x, y st x < 0 & y < 0 holds (the Tran of M . [the InitS of M, [x, y]]) = ( - 1)) holds for x,y be Element of REAL holds ( Result ( [x, y],M)) = ( max (( sgn x),( sgn y)))

    proof

      let M be calculating_type halting non empty Moore-SM_Final over [: REAL , REAL :], ( succ REAL );

      assume that

       A1: the carrier of M = ( succ REAL ) and

       A2: the FinalS of M = REAL and

       A3: the InitS of M = REAL and

       A4: the OFun of M = ( id the carrier of M);

      assume that

       A5: for x, y st x > 0 or y > 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 1 and

       A6: for x, y st (x = 0 or y = 0 ) & x <= 0 & y <= 0 holds (the Tran of M . [the InitS of M, [x, y]]) = 0 and

       A7: for x, y st x < 0 & y < 0 holds (the Tran of M . [the InitS of M, [x, y]]) = ( - 1);

      let x,y be Element of REAL ;

      ( max (( sgn x),( sgn y))) in REAL by XREAL_0:def 1;

      then

       A8: ( max (( sgn x),( sgn y))) in ( succ REAL ) by XBOOLE_0:def 3;

      ( max (( sgn x),( sgn y))) is_result_of ( [x, y],M) by A1, A2, A3, A4, A5, A6, A7, Th26;

      hence thesis by A8, Def9;

    end;