fsm_3.miz



    begin

    reserve x,y,X for set;

    reserve E for non empty set;

    reserve e for Element of E;

    reserve u,u1,v,v1,v2,w,w9,w1,w2 for Element of (E ^omega );

    reserve F for Subset of (E ^omega );

    reserve i,k,l for Nat;

    reserve TS for non empty transition-system over F;

    reserve S,T for Subset of TS;

    theorem :: FSM_3:1

    

     Th1: i >= (k + l) implies i >= k

    proof

      assume i >= (k + l);

      then (i + l) >= ((k + l) + 0 ) by XREAL_1: 7;

      hence thesis by XREAL_1: 6;

    end;

    theorem :: FSM_3:2

    for a,b be FinSequence holds (a ^ b) = a or (b ^ a) = a implies b = {}

    proof

      let a,b be FinSequence such that

       A1: (a ^ b) = a or (b ^ a) = a;

      per cases by A1;

        suppose

         A2: (a ^ b) = a;

        ( len (a ^ b)) = (( len a) + ( len b)) by FINSEQ_1: 22;

        hence thesis by A2;

      end;

        suppose

         A3: (b ^ a) = a;

        ( len (b ^ a)) = (( len b) + ( len a)) by FINSEQ_1: 22;

        hence thesis by A3;

      end;

    end;

    theorem :: FSM_3:3

    

     Th3: for p,q be FinSequence st k in ( dom p) & (( len p) + 1) = ( len q) holds (k + 1) in ( dom q)

    proof

      let p,q be FinSequence such that

       A1: k in ( dom p) and

       A2: (( len p) + 1) = ( len q);

      k <= ( len p) by A1, FINSEQ_3: 25;

      then (1 + 0 ) <= (k + 1) & (k + 1) <= (( len p) + 1) by XREAL_1: 7;

      hence thesis by A2, FINSEQ_3: 25;

    end;

    theorem :: FSM_3:4

    

     Th4: ( len u) = 1 implies ex e st <%e%> = u & e = (u . 0 )

    proof

      assume ( len u) = 1;

      then ( len u) = ( 0 + 1);

      then

      consider v, e such that

       A1: ( len v) = 0 and

       A2: u = (v ^ <%e%>) by FLANG_1: 7;

      take e;

      v = ( <%> E) by A1;

      then u = ( {} ^ <%e%>) by A2;

      then u = <%e%>;

      hence thesis;

    end;

    theorem :: FSM_3:5

    

     Th5: k <> 0 & ( len u) <= (k + 1) implies ex v1, v2 st ( len v1) <= k & ( len v2) <= k & u = (v1 ^ v2)

    proof

      assume that

       A1: k <> 0 and

       A2: ( len u) <= (k + 1);

      per cases ;

        suppose ( len u) = (k + 1);

        then

        consider v1, e such that

         A3: ( len v1) = k and

         A4: u = (v1 ^ <%e%>) by FLANG_1: 7;

        reconsider v2 = <%e%> as Element of (E ^omega );

        take v1, v2;

        thus ( len v1) <= k by A3;

        ( 0 + 1) <= k by A1, NAT_1: 13;

        hence ( len v2) <= k by AFINSQ_1: 34;

        thus u = (v1 ^ v2) by A4;

      end;

        suppose

         A5: ( len u) <> (k + 1);

        reconsider v2 = ( <%> E) as Element of (E ^omega );

        take u, v2;

        thus ( len u) <= k by A2, A5, NAT_1: 8;

        thus ( len v2) <= k;

        

        thus u = (u ^ {} )

        .= (u ^ v2);

      end;

    end;

    theorem :: FSM_3:6

    

     Th6: for p,q be XFinSequence st ( <%x%> ^ p) = ( <%y%> ^ q) holds x = y & p = q

    proof

      let p,q be XFinSequence such that

       A1: ( <%x%> ^ p) = ( <%y%> ^ q);

      (( <%x%> ^ p) . 0 ) = x by AFINSQ_1: 35;

      then x = y by A1, AFINSQ_1: 35;

      hence thesis by A1, AFINSQ_1: 28;

    end;

    theorem :: FSM_3:7

    

     Th7: ( len u) > 0 implies ex e, u1 st u = ( <%e%> ^ u1)

    proof

      assume ( len u) > 0 ;

      then

      consider k such that

       A1: ( len u) = (k + 1) by NAT_1: 6;

      ex u1, e st ( len u1) = k & u = ( <%e%> ^ u1) by A1, FLANG_1: 9;

      hence thesis;

    end;

    registration

      let E;

      cluster ( Lex E) -> non empty;

      coherence

      proof

         <%e%> in ( Lex E) by FLANG_1:def 4;

        hence thesis;

      end;

    end

    theorem :: FSM_3:8

    

     Th8: not ( <%> E) in ( Lex E)

    proof

      assume ( <%> E) in ( Lex E);

      then ex e st e in E & ( <%> E) = <%e%> by FLANG_1:def 4;

      hence contradiction;

    end;

    theorem :: FSM_3:9

    

     Th9: u in ( Lex E) iff ( len u) = 1

    proof

      thus u in ( Lex E) implies ( len u) = 1

      proof

        assume u in ( Lex E);

        then ex e st e in E & u = <%e%> by FLANG_1:def 4;

        hence thesis by AFINSQ_1:def 4;

      end;

      assume ( len u) = 1;

      then ex e st <%e%> = u & e = (u . 0 ) by Th4;

      hence thesis by FLANG_1:def 4;

    end;

    theorem :: FSM_3:10

    

     Th10: u <> v & u in ( Lex E) & v in ( Lex E) implies not ex w st (u ^ w) = v or (w ^ u) = v

    proof

      assume that

       A1: u <> v and

       A2: u in ( Lex E) and

       A3: v in ( Lex E);

      

       A4: ( len u) = 1 by A2, Th9;

      given w such that

       A5: (u ^ w) = v or (w ^ u) = v;

      

       A6: ( len v) = 1 by A3, Th9;

      per cases by A5;

        suppose

         A7: (u ^ w) = v;

        ( len (u ^ w)) = (1 + ( len w)) by A4, AFINSQ_1: 17;

        then w = ( <%> E) by A6, A7;

        hence contradiction by A1, A7;

      end;

        suppose

         A8: (w ^ u) = v;

        ( len (w ^ u)) = (1 + ( len w)) by A4, AFINSQ_1: 17;

        then w = ( <%> E) by A6, A8;

        hence contradiction by A1, A8;

      end;

    end;

    theorem :: FSM_3:11

    

     Th11: for TS be transition-system over ( Lex E) holds the Tran of TS is Function implies TS is deterministic

    proof

      let TS be transition-system over ( Lex E) such that

       A1: the Tran of TS is Function;

       A2:

      now

        let p be Element of TS, u, v such that

         A3: u <> v and

         A4: [p, u] in ( dom the Tran of TS) & [p, v] in ( dom the Tran of TS);

        u in ( Lex E) & v in ( Lex E) by A4, ZFMISC_1: 87;

        hence not ex w st (u ^ w) = v or (v ^ w) = u by A3, Th10;

      end;

       not ( <%> E) in ( rng ( dom the Tran of TS)) by Th8;

      hence thesis by A1, A2, REWRITE3:def 1;

    end;

    definition

      let E, F, TS;

      :: FSM_3:def1

      func _bool TS -> strict transition-system over ( Lex E) means

      : Def1: the carrier of it = ( bool the carrier of TS) & for S, w, T holds [ [S, w], T] in the Tran of it iff ( len w) = 1 & T = (w -succ_of (S,TS));

      existence

      proof

        set cTS = ( bool the carrier of TS);

        defpred P[ set, set] means for c be Element of cTS, i be Element of (E ^omega ) st $1 = [c, i] holds ( len i) = 1 & $2 = (i -succ_of (c,TS));

        consider tTS be Relation of [:cTS, ( Lex E):], cTS such that

         A1: for x be Element of [:cTS, ( Lex E):], y be Element of cTS holds [x, y] in tTS iff P[x, y] from RELSET_1:sch 2;

        set bTS = transition-system (# cTS, tTS #);

        reconsider bTS as strict transition-system over ( Lex E);

        take bTS;

        thus the carrier of bTS = ( bool the carrier of TS);

        let S, w, T;

        thus [ [S, w], T] in the Tran of bTS implies ( len w) = 1 & T = (w -succ_of (S,TS))

        proof

          assume

           A2: [ [S, w], T] in the Tran of bTS;

          then

          reconsider xc = [S, w] as Element of [:cTS, ( Lex E):] by ZFMISC_1: 87;

           [xc, T] in tTS by A2;

          hence thesis by A1;

        end;

        set x = [S, w];

        assume that

         A3: ( len w) = 1 and

         A4: T = (w -succ_of (S,TS));

         A5:

        now

          let xc be Element of cTS, xi be Element of (E ^omega ) such that

           A6: x = [xc, xi];

          xc = S by A6, XTUPLE_0: 1;

          hence ( len xi) = 1 & T = (xi -succ_of (xc,TS)) by A3, A4, A6, XTUPLE_0: 1;

        end;

        w in ( Lex E) by A3, Th9;

        then

        reconsider x as Element of [:cTS, ( Lex E):] by ZFMISC_1: 87;

         [x, T] in tTS by A1, A5;

        hence thesis;

      end;

      uniqueness

      proof

        set cTS = ( bool the carrier of TS);

        let bTS1,bTS2 be strict transition-system over ( Lex E) such that

         A7: the carrier of bTS1 = cTS and

         A8: for S, w, T holds [ [S, w], T] in the Tran of bTS1 iff ( len w) = 1 & T = (w -succ_of (S,TS)) and

         A9: the carrier of bTS2 = cTS and

         A10: for S, w, T holds [ [S, w], T] in the Tran of bTS2 iff ( len w) = 1 & T = (w -succ_of (S,TS));

        

         A11: for x be object holds x in the Tran of bTS2 implies x in the Tran of bTS1

        proof

          let x be object;

          assume

           A12: x in the Tran of bTS2;

          then

          consider xbi,xc be object such that

           A13: x = [xbi, xc] and

           A14: xbi in [:cTS, ( Lex E):] and

           A15: xc in cTS by A9, RELSET_1: 2;

          reconsider xc as Element of cTS by A15;

           [:cTS, ( Lex E):] c= [:cTS, ( Lex E):];

          then

          consider xb,xi be object such that

           A16: xbi = [xb, xi] and

           A17: xb in cTS and

           A18: xi in ( Lex E) by A14, RELSET_1: 2;

          reconsider xb as Element of cTS by A17;

          reconsider xi as Element of ( Lex E) by A18;

          reconsider xe = xi as Element of (E ^omega );

          

           A19: ( len xe) = 1 by Th9;

          xc = (xi -succ_of (xb,TS)) by A10, A12, A13, A16;

          hence thesis by A8, A13, A16, A19;

        end;

        for x be object holds x in the Tran of bTS1 implies x in the Tran of bTS2

        proof

          let x be object;

          assume

           A20: x in the Tran of bTS1;

          then

          consider xbi,xc be object such that

           A21: x = [xbi, xc] and

           A22: xbi in [:cTS, ( Lex E):] and

           A23: xc in cTS by A7, RELSET_1: 2;

          reconsider xc as Element of cTS by A23;

           [:cTS, ( Lex E):] c= [:cTS, ( Lex E):];

          then

          consider xb,xi be object such that

           A24: xbi = [xb, xi] and

           A25: xb in cTS and

           A26: xi in ( Lex E) by A22, RELSET_1: 2;

          reconsider xb as Element of cTS by A25;

          reconsider xi as Element of ( Lex E) by A26;

          reconsider xe = xi as Element of (E ^omega );

          

           A27: ( len xe) = 1 by Th9;

          xc = (xi -succ_of (xb,TS)) by A8, A20, A21, A24;

          hence thesis by A10, A21, A24, A27;

        end;

        hence thesis by A7, A9, A11, TARSKI: 2;

      end;

    end

    registration

      let E, F, TS;

      cluster ( _bool TS) -> non empty deterministic;

      coherence

      proof

        set bTS = ( _bool TS);

        set wTS = the carrier of bTS;

        set tTS = the Tran of bTS;

        for x,y1,y2 be object st [x, y1] in tTS & [x, y2] in tTS holds y1 = y2

        proof

          let x,y1,y2 be object such that

           A1: [x, y1] in tTS and

           A2: [x, y2] in tTS;

          reconsider x as Element of [:wTS, ( Lex E):] by A1, ZFMISC_1: 87;

          reconsider y1, y2 as Element of wTS by A1, A2, ZFMISC_1: 87;

          the carrier of bTS = ( bool the carrier of TS) by Def1;

          then

          consider xc,xi be object such that

           A3: xc in wTS and

           A4: xi in ( Lex E) and

           A5: x = [xc, xi] by ZFMISC_1:def 2;

          reconsider xc as Element of wTS by A3;

          reconsider xi as Element of ( Lex E) by A4;

          reconsider xi as Element of (E ^omega );

          reconsider xc, y1, y2 as Subset of TS by Def1;

          y1 = (xi -succ_of (xc,TS)) & y2 = (xi -succ_of (xc,TS)) by A1, A2, A5, Def1;

          hence thesis;

        end;

        then

         A6: the Tran of bTS is Function by FUNCT_1:def 1;

        the carrier of bTS = ( bool the carrier of TS) by Def1;

        hence thesis by A6, Th11;

      end;

    end

    registration

      let E, F;

      let TS be finite non empty transition-system over F;

      cluster ( _bool TS) -> finite;

      coherence

      proof

        ( bool the carrier of TS) is finite;

        hence thesis by Def1;

      end;

    end

    theorem :: FSM_3:12

    

     Th12: (x, <%e%>) ==>* (y,( <%> E),( _bool TS)) implies (x, <%e%>) ==>. (y,( <%> E),( _bool TS))

    proof

       not ( <%> E) in ( rng ( dom the Tran of ( _bool TS))) by REWRITE3:def 1;

      hence thesis by REWRITE3: 92;

    end;

    theorem :: FSM_3:13

    

     Th13: ( len w) = 1 implies (X = (w -succ_of (S,TS)) iff (S,w) ==>* (X,( _bool TS)))

    proof

      assume

       A1: ( len w) = 1;

      thus X = (w -succ_of (S,TS)) implies (S,w) ==>* (X,( _bool TS))

      proof

        assume X = (w -succ_of (S,TS));

        then [ [S, w], X] in the Tran of ( _bool TS) by A1, Def1;

        then (S,w) -->. (X,( _bool TS)) by REWRITE3:def 2;

        then (S,w) ==>. (X,( <%> E),( _bool TS)) by REWRITE3: 23;

        then (S,w) ==>* (X,( <%> E),( _bool TS)) by REWRITE3: 87;

        hence thesis by REWRITE3:def 7;

      end;

      assume (S,w) ==>* (X,( _bool TS));

      then

       A2: (S,w) ==>* (X,( <%> E),( _bool TS)) by REWRITE3:def 7;

      ex e st w = <%e%> & (w . 0 ) = e by A1, Th4;

      then (S,(w ^ {} )) ==>. (X,( <%> E),( _bool TS)) by A2, Th12;

      then

       A3: (S,w) -->. (X,( _bool TS)) by REWRITE3: 24;

      then X in ( _bool TS) by REWRITE3: 15;

      then X in the carrier of ( _bool TS);

      then

      reconsider X9 = X as Subset of TS by Def1;

       [ [S, w], X9] in the Tran of ( _bool TS) by A3, REWRITE3:def 2;

      hence thesis by Def1;

    end;

    definition

      let E, F;

      struct ( transition-system over F) semiautomaton over F (# the carrier -> set,

the Tran -> Relation of [: the carrier, F:], the carrier,

the InitS -> Subset of the carrier #)

       attr strict strict;

    end

    definition

      let E, F;

      let SA be semiautomaton over E, F;

      :: FSM_3:def2

      attr SA is deterministic means

      : Def2: the transition-system of SA is deterministic & ( card the InitS of SA) = 1;

    end

    registration

      let E, F;

      cluster strict non empty finite deterministic for semiautomaton over E, F;

      existence

      proof

        set X = the non empty finite set;

        reconsider T = {} as Relation of [:X, F:], X by RELSET_1: 12;

        set x = the Element of X;

        reconsider I = {x} as Subset of X;

        take SA = semiautomaton (# X, T, I #);

        thus SA is strict;

        thus SA is non empty;

        thus the carrier of SA is finite;

        thus the transition-system of SA is deterministic by RELAT_1: 38, REWRITE3: 14;

        thus ( card the InitS of SA) = 1 by CARD_1: 30;

      end;

    end

    reserve SA for non empty semiautomaton over E, F;

    registration

      let E, F, SA;

      cluster the transition-system of SA -> non empty;

      coherence ;

    end

    definition

      let E, F, SA;

      :: FSM_3:def3

      func _bool SA -> strict semiautomaton over E, ( Lex E) means

      : Def3: the transition-system of it = ( _bool the transition-system of SA) & the InitS of it = {(( <%> E) -succ_of (the InitS of SA,SA))};

      existence

      proof

        reconsider TS = the transition-system of SA as non empty transition-system over F;

        set cSA = the carrier of ( _bool TS);

        reconsider iSA = {(( <%> E) -succ_of (the InitS of SA,SA))} as Subset of cSA by Def1;

        reconsider tSA = the Tran of ( _bool TS) as Relation of [:cSA, ( Lex E):], cSA;

        set bSA = semiautomaton (# cSA, tSA, iSA #);

        ( card iSA) = 1 by CARD_1: 30;

        then

        reconsider bSA as strict non empty deterministic semiautomaton over E, ( Lex E) by Def2;

        take bSA;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let E, F, SA;

      cluster ( _bool SA) -> non empty deterministic;

      coherence

      proof

        set TS = ( _bool SA);

        the InitS of TS = {(( <%> E) -succ_of (the InitS of SA,SA))} by Def3;

        then

         A1: ( card the InitS of TS) = 1 by CARD_1: 30;

         the transition-system of TS = ( _bool the transition-system of SA) by Def3;

        hence thesis by A1;

      end;

    end

    theorem :: FSM_3:14

    

     Th14: the carrier of ( _bool SA) = ( bool the carrier of SA)

    proof

       the transition-system of ( _bool SA) = ( _bool the transition-system of SA) by Def3;

      hence thesis by Def1;

    end;

    registration

      let E, F;

      let SA be finite non empty semiautomaton over E, F;

      cluster ( _bool SA) -> finite;

      coherence

      proof

        ( bool the carrier of SA) is finite;

        hence thesis by Th14;

      end;

    end

    definition

      let E, F, SA;

      let Q be Subset of SA;

      :: FSM_3:def4

      func left-Lang (Q) -> Subset of (E ^omega ) equals { w : Q meets (w -succ_of (the InitS of SA,SA)) };

      coherence

      proof

        defpred P[ Element of (E ^omega )] means Q meets ($1 -succ_of (the InitS of SA,SA));

        { w : P[w] } c= (E ^omega ) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: FSM_3:15

    

     Th15: for Q be Subset of SA holds w in ( left-Lang Q) iff Q meets (w -succ_of (the InitS of SA,SA))

    proof

      let Q be Subset of SA;

      thus w in ( left-Lang Q) implies Q meets (w -succ_of (the InitS of SA,SA))

      proof

        assume w in ( left-Lang Q);

        then ex w9 st w9 = w & Q meets (w9 -succ_of (the InitS of SA,SA));

        hence thesis;

      end;

      thus thesis;

    end;

    definition

      let E, F;

      struct ( semiautomaton over E, F) automaton over F (# the carrier -> set,

the Tran -> Relation of [: the carrier, F:], the carrier,

the InitS -> Subset of the carrier,

the FinalS -> Subset of the carrier #)

       attr strict strict;

    end

    definition

      let E, F;

      let A be automaton over E, F;

      :: FSM_3:def5

      attr A is deterministic means

      : Def5: the semiautomaton of A is deterministic;

    end

    registration

      let E, F;

      cluster strict non empty finite deterministic for automaton over E, F;

      existence

      proof

        set X = the non empty finite set;

        reconsider T = {} as Relation of [:X, F:], X by RELSET_1: 12;

        set x = the Element of X;

        reconsider I = {x} as Subset of X;

        take A = automaton (# X, T, I, I #);

        thus A is strict;

        thus A is non empty;

        thus the carrier of A is finite;

         the transition-system of A is deterministic & ( card the InitS of A) = 1 by CARD_1: 30, RELAT_1: 38, REWRITE3: 14;

        then the semiautomaton of A is deterministic;

        hence A is deterministic;

      end;

    end

    reserve A for non empty automaton over E, F;

    reserve p,q for Element of A;

    registration

      let E, F, A;

      cluster the transition-system of A -> non empty;

      coherence ;

      cluster the semiautomaton of A -> non empty;

      coherence ;

    end

    definition

      let E, F, A;

      :: FSM_3:def6

      func _bool A -> strict automaton over E, ( Lex E) means

      : Def6: the semiautomaton of it = ( _bool the semiautomaton of A) & the FinalS of it = { Q where Q be Element of it : Q meets the FinalS of A };

      existence

      proof

        reconsider SA = the semiautomaton of A as non empty semiautomaton over E, F;

        set cA = the carrier of ( _bool SA);

        reconsider tA = the Tran of ( _bool SA) as Relation of [:cA, ( Lex E):], cA;

        set iA = the InitS of ( _bool SA);

        { Q where Q be Element of ( _bool SA) : Q meets the FinalS of A } is Subset of cA

        proof

          defpred P[ set] means $1 meets the FinalS of A;

          { Q where Q be Element of ( _bool SA) : P[Q] } c= the carrier of ( _bool SA) from FRAENKEL:sch 10;

          hence thesis;

        end;

        then

        reconsider fA = { Q where Q be Element of ( _bool SA) : Q meets the FinalS of A } as Subset of cA;

        set bA = automaton (# cA, tA, iA, fA #);

        reconsider bA as strict non empty deterministic automaton over E, ( Lex E) by Def5;

        take bA;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let E, F, A;

      cluster ( _bool A) -> non empty deterministic;

      coherence

      proof

        set XX = ( _bool A);

         the semiautomaton of XX = ( _bool the semiautomaton of A) by Def6;

        hence thesis;

      end;

    end

    theorem :: FSM_3:16

    

     Th16: the carrier of ( _bool A) = ( bool the carrier of A)

    proof

       the semiautomaton of ( _bool A) = ( _bool the semiautomaton of A) by Def6;

      hence thesis by Th14;

    end;

    registration

      let E, F;

      let A be finite non empty automaton over E, F;

      cluster ( _bool A) -> finite;

      coherence

      proof

        ( bool the carrier of A) is finite;

        hence thesis by Th16;

      end;

    end

    definition

      let E, F, A;

      let Q be Subset of A;

      :: FSM_3:def7

      func right-Lang (Q) -> Subset of (E ^omega ) equals { w : (w -succ_of (Q,A)) meets the FinalS of A };

      coherence

      proof

        defpred P[ Element of (E ^omega )] means ($1 -succ_of (Q,A)) meets the FinalS of A;

        { w : P[w] } c= (E ^omega ) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: FSM_3:17

    

     Th17: for Q be Subset of A holds w in ( right-Lang Q) iff (w -succ_of (Q,A)) meets the FinalS of A

    proof

      let Q be Subset of A;

      thus w in ( right-Lang Q) implies (w -succ_of (Q,A)) meets the FinalS of A

      proof

        assume w in ( right-Lang Q);

        then ex w9 st w = w9 & (w9 -succ_of (Q,A)) meets the FinalS of A;

        hence thesis;

      end;

      thus thesis;

    end;

    definition

      let E, F, A;

      :: FSM_3:def8

      func Lang (A) -> Subset of (E ^omega ) equals { u : ex p, q st p in the InitS of A & q in the FinalS of A & (p,u) ==>* (q,A) };

      coherence

      proof

        defpred P[ Element of (E ^omega )] means ex p, q st p in the InitS of A & q in the FinalS of A & (p,$1) ==>* (q,A);

        { w : P[w] } c= (E ^omega ) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: FSM_3:18

    

     Th18: w in ( Lang A) iff ex p, q st p in the InitS of A & q in the FinalS of A & (p,w) ==>* (q,A)

    proof

      thus w in ( Lang A) implies ex p, q st p in the InitS of A & q in the FinalS of A & (p,w) ==>* (q,A)

      proof

        assume w in ( Lang A);

        then ex u st w = u & ex p, q st p in the InitS of A & q in the FinalS of A & (p,u) ==>* (q,A);

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: FSM_3:19

    

     Th19: w in ( Lang A) iff (w -succ_of (the InitS of A,A)) meets the FinalS of A

    proof

      thus w in ( Lang A) implies (w -succ_of (the InitS of A,A)) meets the FinalS of A

      proof

        assume w in ( Lang A);

        then

        consider p, q such that

         A1: p in the InitS of A and

         A2: q in the FinalS of A and

         A3: (p,w) ==>* (q,A) by Th18;

        q in (w -succ_of (the InitS of A,A)) by A1, A3, REWRITE3: 103;

        hence thesis by A2, XBOOLE_0: 3;

      end;

      assume (w -succ_of (the InitS of A,A)) meets the FinalS of A;

      then

      consider x be object such that

       A4: x in (w -succ_of (the InitS of A,A)) and

       A5: x in the FinalS of A by XBOOLE_0: 3;

      reconsider x as Element of A by A4;

      ex p st p in the InitS of A & (p,w) ==>* (x,A) by A4, REWRITE3: 103;

      hence thesis by A5;

    end;

    theorem :: FSM_3:20

    ( Lang A) = ( left-Lang the FinalS of A)

    proof

      

       A1: w in ( Lang A) implies w in ( left-Lang the FinalS of A)

      proof

        assume w in ( Lang A);

        then (w -succ_of (the InitS of A,A)) meets the FinalS of A by Th19;

        hence thesis;

      end;

      w in ( left-Lang the FinalS of A) implies w in ( Lang A)

      proof

        assume w in ( left-Lang the FinalS of A);

        then the FinalS of A meets (w -succ_of (the InitS of A,A)) by Th15;

        hence thesis by Th19;

      end;

      hence thesis by A1, SUBSET_1: 3;

    end;

    theorem :: FSM_3:21

    ( Lang A) = ( right-Lang the InitS of A)

    proof

      

       A1: w in ( Lang A) implies w in ( right-Lang the InitS of A)

      proof

        assume w in ( Lang A);

        then (w -succ_of (the InitS of A,A)) meets the FinalS of A by Th19;

        hence thesis;

      end;

      w in ( right-Lang the InitS of A) implies w in ( Lang A)

      proof

        assume w in ( right-Lang the InitS of A);

        then (w -succ_of (the InitS of A,A)) meets the FinalS of A by Th17;

        hence thesis by Th19;

      end;

      hence thesis by A1, SUBSET_1: 3;

    end;

    reserve TS for non empty transition-system over (( Lex E) \/ {( <%> E)});

    theorem :: FSM_3:22

    

     Th22: for R be RedSequence of ( ==>.-relation TS) st ((R . 1) `2 ) = ( <%e%> ^ u) & ((R . ( len R)) `2 ) = ( <%> E) holds ((R . 2) `2 ) = ( <%e%> ^ u) or ((R . 2) `2 ) = u

    proof

      let R be RedSequence of ( ==>.-relation TS) such that

       A1: ((R . 1) `2 ) = ( <%e%> ^ u) and

       A2: ((R . ( len R)) `2 ) = ( <%> E);

      ((R . 1) `2 ) <> ((R . ( len R)) `2 ) by A1, A2, AFINSQ_1: 30;

      then ( len R) >= (1 + 1) by NAT_1: 8, NAT_1: 25;

      then ( rng R) <> {} & (1 + 1) in ( dom R) by FINSEQ_3: 25;

      then

       A3: [(R . 1), (R . 2)] in ( ==>.-relation TS) by FINSEQ_3: 32, REWRITE1:def 2;

      then

      consider p be Element of TS, v be Element of (E ^omega ), q be Element of TS, w such that

       A4: (R . 1) = [p, v] and

       A5: (R . 2) = [q, w] by REWRITE3: 31;

      (p,v) ==>. (q,w,TS) by A3, A4, A5, REWRITE3:def 4;

      then

      consider u1 such that

       A6: (p,u1) -->. (q,TS) and

       A7: v = (u1 ^ w) by REWRITE3: 22;

      

       A8: u1 in (( Lex E) \/ {( <%> E)}) by A6, REWRITE3: 15;

      per cases by A8, XBOOLE_0:def 3;

        suppose u1 in ( Lex E);

        then ( len u1) = 1 by Th9;

        then

        consider f be Element of E such that

         A9: u1 = <%f%> and (u1 . 0 ) = f by Th4;

        ((R . 1) `2 ) = ( <%f%> ^ w) by A4, A7, A9;

        then u = w by A1, Th6;

        hence thesis by A5;

      end;

        suppose u1 in {( <%> E)};

        then

         A10: u1 = ( <%> E) by TARSKI:def 1;

        v = ((R . 1) `2 ) & w = ((R . 2) `2 ) by A4, A5;

        hence thesis by A1, A7, A10;

      end;

    end;

    theorem :: FSM_3:23

    

     Th23: for R be RedSequence of ( ==>.-relation TS) st ((R . 1) `2 ) = u & ((R . ( len R)) `2 ) = ( <%> E) holds ( len R) > ( len u)

    proof

      defpred P[ Nat] means for R be RedSequence of ( ==>.-relation TS), u st ( len R) = $1 & ((R . 1) `2 ) = u & ((R . ( len R)) `2 ) = ( <%> E) holds ( len R) > ( len u);

       A1:

      now

        let k;

        assume

         A2: P[k];

        now

          let R be RedSequence of ( ==>.-relation TS), u such that

           A3: ( len R) = (k + 1) and

           A4: ((R . 1) `2 ) = u and

           A5: ((R . ( len R)) `2 ) = ( <%> E);

          per cases ;

            suppose ( len u) = 0 ;

            hence ( len R) > ( len u);

          end;

            suppose

             A6: ( len u) > 0 ;

            then

            consider e, u1 such that

             A7: u = ( <%e%> ^ u1) by Th7;

            ( len R) <> 1 by A4, A5, A6;

            then

            consider R9 be RedSequence of ( ==>.-relation TS) such that

             A8: ( <*(R . 1)*> ^ R9) = R and

             A9: (( len R9) + 1) = ( len R) by NAT_1: 25, REWRITE3: 5;

            

             A10: (( len R9) + 0 ) < (k + 1) by A3, A9, XREAL_1: 6;

            

             A11: ( len R9) >= ( 0 + 1) by NAT_1: 8;

            then ( len R9) in ( dom R9) by FINSEQ_3: 25;

            then

             A12: ((R9 . ( len R9)) `2 ) = ( <%> E) by A5, A8, A9, REWRITE3: 1;

            1 in ( dom R9) by A11, FINSEQ_3: 25;

            then

             A13: (( <*(R . 1)*> ^ R9) . (1 + 1)) = (R9 . 1) by REWRITE3: 1;

            per cases by A4, A5, A7, Th22;

              suppose ((R . 2) `2 ) = ( <%e%> ^ u1);

              hence ( len R) > ( len u) by A2, A3, A7, A8, A9, A10, A13, A12, XXREAL_0: 2;

            end;

              suppose ((R . 2) `2 ) = u1;

              then ( len R9) > ( len u1) by A2, A3, A8, A9, A13, A12;

              then ( len R) > (1 + ( len u1)) by A9, XREAL_1: 6;

              then ( len R) > (( len <%e%>) + ( len u1)) by AFINSQ_1:def 4;

              hence ( len R) > ( len u) by A7, AFINSQ_1: 17;

            end;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A14: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A14, A1);

      hence thesis;

    end;

    theorem :: FSM_3:24

    

     Th24: for R be RedSequence of ( ==>.-relation TS) st ((R . 1) `2 ) = (u ^ v) & ((R . ( len R)) `2 ) = ( <%> E) holds ex l st l in ( dom R) & ((R . l) `2 ) = v

    proof

      defpred P[ Nat] means for R be RedSequence of ( ==>.-relation TS), u st ( len R) = $1 & ((R . 1) `2 ) = (u ^ v) & ((R . ( len R)) `2 ) = ( <%> E) holds ex l st l in ( dom R) & ((R . l) `2 ) = v;

       A1:

      now

        let i;

        assume

         A2: P[i];

        thus P[(i + 1)]

        proof

          let R be RedSequence of ( ==>.-relation TS), u such that

           A3: ( len R) = (i + 1) and

           A4: ((R . 1) `2 ) = (u ^ v) and

           A5: ((R . ( len R)) `2 ) = ( <%> E);

          per cases ;

            suppose

             A6: ( len u) = 0 ;

            set j = 1;

            take j;

            ( rng R) <> {} ;

            hence j in ( dom R) by FINSEQ_3: 32;

            u = {} by A6;

            hence ((R . j) `2 ) = v by A4;

          end;

            suppose

             A7: ( len u) > 0 ;

            then

            consider e, u1 such that

             A8: u = ( <%e%> ^ u1) by Th7;

            ( len u) >= ( 0 + 1) by A7, NAT_1: 13;

            then (( len u) + ( len v)) >= (1 + ( len v)) by XREAL_1: 6;

            then ( len (u ^ v)) >= (1 + ( len v)) by AFINSQ_1: 17;

            then ( len (u ^ v)) >= 1 by Th1;

            then (( len R) + ( len (u ^ v))) > (( len (u ^ v)) + 1) by A4, A5, Th23, XREAL_1: 8;

            then ( len R) > 1 by XREAL_1: 6;

            then

            consider R9 be RedSequence of ( ==>.-relation TS) such that

             A9: (( len R9) + 1) = ( len R) and

             A10: for k st k in ( dom R9) holds (R9 . k) = (R . (k + 1)) by REWRITE3: 7;

            

             A11: ( rng R9) <> {} ;

            then

             A12: ((R9 . 1) `2 ) = ((R . (1 + 1)) `2 ) by A10, FINSEQ_3: 32;

            1 in ( dom R9) by A11, FINSEQ_3: 32;

            then 1 <= ( len R9) by FINSEQ_3: 25;

            then ( len R9) in ( dom R9) by FINSEQ_3: 25;

            then

             A13: ((R9 . ( len R9)) `2 ) = ( <%> E) by A5, A9, A10;

            

             A14: ((R . 1) `2 ) = ( <%e%> ^ (u1 ^ v)) by A4, A8, AFINSQ_1: 27;

            thus ex k st k in ( dom R) & ((R . k) `2 ) = v

            proof

              per cases by A4, A5, A14, Th22;

                suppose ((R . 2) `2 ) = (u ^ v);

                then

                consider l such that

                 A15: l in ( dom R9) and

                 A16: ((R9 . l) `2 ) = v by A2, A3, A9, A12, A13;

                set k = (l + 1);

                take k;

                thus k in ( dom R) by A9, A15, Th3;

                thus ((R . k) `2 ) = v by A10, A15, A16;

              end;

                suppose ((R . 2) `2 ) = (u1 ^ v);

                then

                consider l such that

                 A17: l in ( dom R9) and

                 A18: ((R9 . l) `2 ) = v by A2, A3, A9, A12, A13;

                set k = (l + 1);

                take k;

                thus k in ( dom R) by A9, A17, Th3;

                thus ((R . k) `2 ) = v by A10, A17, A18;

              end;

            end;

          end;

        end;

      end;

      

       A19: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A19, A1);

      hence thesis;

    end;

    definition

      let E, u, v;

      :: FSM_3:def9

      func chop (u,v) -> Element of (E ^omega ) means

      : Def9: for w st (w ^ v) = u holds it = w if ex w st (w ^ v) = u

      otherwise it = u;

      existence

      proof

        thus (ex w st (w ^ v) = u) implies ex w1 st for w st (w ^ v) = u holds w1 = w

        proof

          given w1 such that

           A1: (w1 ^ v) = u;

          take w1;

          let w;

          assume (w ^ v) = u;

          hence w1 = w by A1, AFINSQ_1: 28;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let w1, w2;

        hereby

          given w such that

           A2: (w ^ v) = u;

          assume that

           A3: for w st (w ^ v) = u holds w1 = w and

           A4: for w st (w ^ v) = u holds w2 = w;

          w1 = w by A2, A3;

          hence w1 = w2 by A2, A4;

        end;

        thus thesis;

      end;

      consistency ;

    end

    theorem :: FSM_3:25

    

     Th25: for p be RedSequence of ( ==>.-relation TS) st (p . 1) = [x, (u ^ w)] & (p . ( len p)) = [y, (v ^ w)] holds ex q be RedSequence of ( ==>.-relation TS) st (q . 1) = [x, u] & (q . ( len q)) = [y, v]

    proof

      let p be RedSequence of ( ==>.-relation TS) such that

       A1: (p . 1) = [x, (u ^ w)] and

       A2: (p . ( len p)) = [y, (v ^ w)];

      

       A3: ( len p) >= ( 0 + 1) by NAT_1: 13;

      then 1 in ( dom p) by FINSEQ_3: 25;

      

      then

       A4: ( dim2 ((p . 1),E)) = ((p . 1) `2 ) by A1, REWRITE3: 51

      .= (u ^ w) by A1;

      deffunc F( set) = [((p . $1) `1 ), ( chop (( dim2 ((p . $1),E)),w))];

      consider q be FinSequence such that

       A5: ( len q) = ( len p) and

       A6: for k st k in ( dom q) holds (q . k) = F(k) from FINSEQ_1:sch 2;

      

       A7: for k be Nat st k in ( dom q) & (k + 1) in ( dom q) holds [(q . k), (q . (k + 1))] in ( ==>.-relation TS)

      proof

        let k be Nat such that

         A8: k in ( dom q) and

         A9: (k + 1) in ( dom q);

        1 <= k & k <= ( len q) by A8, FINSEQ_3: 25;

        then

         A10: k in ( dom p) by A5, FINSEQ_3: 25;

        then

        consider v1 such that

         A11: ((p . k) `2 ) = (v1 ^ (v ^ w)) by A2, REWRITE3: 52;

        1 <= (k + 1) & (k + 1) <= ( len q) by A9, FINSEQ_3: 25;

        then

         A12: (k + 1) in ( dom p) by A5, FINSEQ_3: 25;

        then

        consider v2 such that

         A13: ((p . (k + 1)) `2 ) = (v2 ^ (v ^ w)) by A2, REWRITE3: 52;

        

         A14: [(p . k), (p . (k + 1))] in ( ==>.-relation TS) by A10, A12, REWRITE1:def 2;

        then [(p . k), [((p . (k + 1)) `1 ), (v2 ^ (v ^ w))]] in ( ==>.-relation TS) by A10, A12, A13, REWRITE3: 48;

        then [ [((p . k) `1 ), (v1 ^ (v ^ w))], [((p . (k + 1)) `1 ), (v2 ^ (v ^ w))]] in ( ==>.-relation TS) by A10, A12, A11, REWRITE3: 48;

        then (((p . k) `1 ),(v1 ^ (v ^ w))) ==>. (((p . (k + 1)) `1 ),(v2 ^ (v ^ w)),TS) by REWRITE3:def 4;

        then

        consider u1 such that

         A15: (((p . k) `1 ),u1) -->. (((p . (k + 1)) `1 ),TS) and

         A16: (v1 ^ (v ^ w)) = (u1 ^ (v2 ^ (v ^ w))) by REWRITE3: 22;

        

         A17: ex r1 be Element of TS, w1 be Element of (E ^omega ), r2 be Element of TS, w2 st (p . k) = [r1, w1] & (p . (k + 1)) = [r2, w2] by A14, REWRITE3: 31;

        then ( dim2 ((p . (k + 1)),E)) = (v2 ^ (v ^ w)) by A13, REWRITE3:def 5;

        

        then

         A18: (q . (k + 1)) = [((p . (k + 1)) `1 ), ( chop ((v2 ^ (v ^ w)),w))] by A6, A9

        .= [((p . (k + 1)) `1 ), ( chop (((v2 ^ v) ^ w),w))] by AFINSQ_1: 27

        .= [((p . (k + 1)) `1 ), (v2 ^ v)] by Def9;

        ((v1 ^ v) ^ w) = (u1 ^ (v2 ^ (v ^ w))) by A16, AFINSQ_1: 27

        .= ((u1 ^ v2) ^ (v ^ w)) by AFINSQ_1: 27

        .= (((u1 ^ v2) ^ v) ^ w) by AFINSQ_1: 27;

        

        then (v1 ^ v) = ((u1 ^ v2) ^ v) by AFINSQ_1: 28

        .= (u1 ^ (v2 ^ v)) by AFINSQ_1: 27;

        then

         A19: (((p . k) `1 ),(v1 ^ v)) ==>. (((p . (k + 1)) `1 ),(v2 ^ v),TS) by A15, REWRITE3:def 3;

        ( dim2 ((p . k),E)) = (v1 ^ (v ^ w)) by A11, A17, REWRITE3:def 5;

        

        then (q . k) = [((p . k) `1 ), ( chop ((v1 ^ (v ^ w)),w))] by A6, A8

        .= [((p . k) `1 ), ( chop (((v1 ^ v) ^ w),w))] by AFINSQ_1: 27

        .= [((p . k) `1 ), (v1 ^ v)] by Def9;

        hence thesis by A19, A18, REWRITE3:def 4;

      end;

      ( len p) in ( dom p) by A3, FINSEQ_3: 25;

      

      then

       A20: ( dim2 ((p . ( len p)),E)) = ((p . ( len p)) `2 ) by A1, REWRITE3: 51

      .= (v ^ w) by A2;

      reconsider q as RedSequence of ( ==>.-relation TS) by A5, A7, REWRITE1:def 2;

      1 in ( dom q) by A5, A3, FINSEQ_3: 25;

      

      then

       A21: (q . 1) = [((p . 1) `1 ), ( chop (( dim2 ((p . 1),E)),w))] by A6

      .= [x, ( chop ((u ^ w),w))] by A1, A4

      .= [x, u] by Def9;

      ( len p) in ( dom q) by A5, A3, FINSEQ_3: 25;

      

      then (q . ( len q)) = [((p . ( len p)) `1 ), ( chop (( dim2 ((p . ( len p)),E)),w))] by A5, A6

      .= [y, ( chop ((v ^ w),w))] by A2, A20

      .= [y, v] by Def9;

      hence thesis by A21;

    end;

    theorem :: FSM_3:26

    

     Th26: ( ==>.-relation TS) reduces ( [x, (u ^ w)], [y, (v ^ w)]) implies ( ==>.-relation TS) reduces ( [x, u], [y, v])

    proof

      assume ( ==>.-relation TS) reduces ( [x, (u ^ w)], [y, (v ^ w)]);

      then ex p be RedSequence of ( ==>.-relation TS) st (p . 1) = [x, (u ^ w)] & (p . ( len p)) = [y, (v ^ w)] by REWRITE1:def 3;

      then ex q be RedSequence of ( ==>.-relation TS) st (q . 1) = [x, u] & (q . ( len q)) = [y, v] by Th25;

      hence thesis by REWRITE1:def 3;

    end;

    theorem :: FSM_3:27

    

     Th27: (x,(u ^ w)) ==>* (y,(v ^ w),TS) implies (x,u) ==>* (y,v,TS)

    proof

      assume (x,(u ^ w)) ==>* (y,(v ^ w),TS);

      then ( ==>.-relation TS) reduces ( [x, (u ^ w)], [y, (v ^ w)]) by REWRITE3:def 6;

      then ( ==>.-relation TS) reduces ( [x, u], [y, v]) by Th26;

      hence thesis by REWRITE3:def 6;

    end;

    theorem :: FSM_3:28

    

     Th28: for p,q be Element of TS st (p,(u ^ v)) ==>* (q,TS) holds ex r be Element of TS st (p,u) ==>* (r,TS) & (r,v) ==>* (q,TS)

    proof

      let p,q be Element of TS;

      assume

       A1: (p,(u ^ v)) ==>* (q,TS);

      then (p,(u ^ v)) ==>* (q,( <%> E),TS) by REWRITE3:def 7;

      then ( ==>.-relation TS) reduces ( [p, (u ^ v)], [q, ( <%> E)]) by REWRITE3:def 6;

      then

      consider R be RedSequence of ( ==>.-relation TS) such that

       A2: (R . 1) = [p, (u ^ v)] and

       A3: (R . ( len R)) = [q, ( <%> E)] by REWRITE1:def 3;

      

       A4: ((R . ( len R)) `2 ) = ( <%> E) by A3;

      ((R . 1) `2 ) = (u ^ v) by A2;

      then

      consider l such that

       A5: l in ( dom R) and

       A6: ((R . l) `2 ) = v by A4, Th24;

      per cases ;

        suppose

         A7: (l + 1) in ( dom R);

        then ((R . l) `1 ) in TS by A5, REWRITE3: 49;

        then

        reconsider r = ((R . l) `1 ) as Element of TS;

        

         A8: (R . l) = [r, v] by A5, A6, A7, REWRITE3: 48;

        

         A9: l <= ( len R) by A5, FINSEQ_3: 25;

        take r;

        

         A10: 1 in ( dom R) & 1 <= l by A5, FINSEQ_3: 25, FINSEQ_5: 6;

        reconsider l as Element of NAT by ORDINAL1:def 12;

        ( ==>.-relation TS) reduces ((R . 1),(R . l)) by A5, A10, REWRITE1: 17;

        then (p,(u ^ v)) ==>* (r,( {} ^ v),TS) by A2, A8, REWRITE3:def 6;

        then (p,u) ==>* (r,( <%> E),TS) by Th27;

        hence (p,u) ==>* (r,TS) by REWRITE3:def 7;

        ( 0 + 1) <= ( len R) by NAT_1: 13;

        then ( len R) in ( dom R) by FINSEQ_3: 25;

        then ( ==>.-relation TS) reduces ((R . l),(R . ( len R))) by A5, A9, REWRITE1: 17;

        then (r,v) ==>* (q,( <%> E),TS) by A3, A8, REWRITE3:def 6;

        hence (r,v) ==>* (q,TS) by REWRITE3:def 7;

      end;

        suppose not (l + 1) in ( dom R);

        then

         A11: v = ( <%> E) by A4, A5, A6, REWRITE3: 3;

        thus thesis by A1, A11, REWRITE3: 95;

      end;

    end;

    theorem :: FSM_3:29

    

     Th29: ((w ^ v) -succ_of (X,TS)) = (v -succ_of ((w -succ_of (X,TS)),TS))

    proof

       A1:

      now

        let x be object;

        assume

         A2: x in (v -succ_of ((w -succ_of (X,TS)),TS));

        then

        reconsider r = x as Element of TS;

        consider p be Element of TS such that

         A3: p in (w -succ_of (X,TS)) and

         A4: (p,v) ==>* (r,TS) by A2, REWRITE3: 103;

        consider q be Element of TS such that

         A5: q in X and

         A6: (q,w) ==>* (p,TS) by A3, REWRITE3: 103;

        (q,(w ^ v)) ==>* (r,TS) by A4, A6, REWRITE3: 99;

        hence x in ((w ^ v) -succ_of (X,TS)) by A5, REWRITE3: 103;

      end;

      now

        let x be object;

        assume

         A7: x in ((w ^ v) -succ_of (X,TS));

        then

        reconsider r = x as Element of TS;

        consider q be Element of TS such that

         A8: q in X and

         A9: (q,(w ^ v)) ==>* (r,TS) by A7, REWRITE3: 103;

        consider p be Element of TS such that

         A10: (q,w) ==>* (p,TS) and

         A11: (p,v) ==>* (r,TS) by A9, Th28;

        p in (w -succ_of (X,TS)) by A8, A10, REWRITE3: 103;

        hence x in (v -succ_of ((w -succ_of (X,TS)),TS)) by A11, REWRITE3: 103;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: FSM_3:30

    

     Th30: ( _bool TS) is non empty transition-system over (( Lex E) \/ {( <%> E)})

    proof

      ( Lex E) c= (( Lex E) \/ {( <%> E)}) by XBOOLE_1: 7;

      then ( dom the Tran of ( _bool TS)) c= [:the carrier of ( _bool TS), ( Lex E):] & [:the carrier of ( _bool TS), ( Lex E):] c= [:the carrier of ( _bool TS), (( Lex E) \/ {( <%> E)}):] by ZFMISC_1: 95;

      hence thesis by RELSET_1: 5, XBOOLE_1: 1;

    end;

    theorem :: FSM_3:31

    

     Th31: (w -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ w) -succ_of (X,TS))}

    proof

      defpred P[ Nat] means ( len u) <= $1 implies for v holds (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ u) -succ_of (X,TS))};

      

       A1: not ( <%> E) in ( rng ( dom the Tran of ( _bool TS))) by Th8;

      

       A2: P[ 0 ]

      proof

        let u;

        assume ( len u) <= 0 ;

        then

         A3: u = ( <%> E);

        let v;

        reconsider vso = {(v -succ_of (X,TS))} as Subset of ( _bool TS) by Def1;

        (u -succ_of (vso,( _bool TS))) = vso by A1, A3, REWRITE3: 104;

        

        hence (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ {} ) -succ_of (X,TS))}

        .= {((v ^ {} ) -succ_of (X,TS))}

        .= {((v ^ u) -succ_of (X,TS))} by A3;

      end;

       A4:

      now

        let k;

        assume

         A5: P[k];

        now

          let u;

          assume

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

          let v;

          per cases ;

            suppose

             A7: k = 0 ;

            per cases by A6, A7, NAT_1: 25;

              suppose ( len u) = 0 ;

              hence (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ u) -succ_of (X,TS))} by A2;

            end;

              suppose

               A8: ( len u) = 1;

               A9:

              now

                let x be object;

                assume

                 A10: x in {((v ^ u) -succ_of (X,TS))};

                then

                reconsider P = x as Element of ( _bool TS) by Def1;

                x = ((v ^ u) -succ_of (X,TS)) by A10, TARSKI:def 1;

                then x = (u -succ_of ((v -succ_of (X,TS)),TS)) by Th29;

                then

                 A11: ((v -succ_of (X,TS)),u) ==>* (x,( _bool TS)) by A8, Th13;

                (v -succ_of (X,TS)) is Element of ( _bool TS) & (v -succ_of (X,TS)) in {(v -succ_of (X,TS))} by Def1, TARSKI:def 1;

                then P in (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) by A11, REWRITE3: 103;

                hence x in (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS)));

              end;

              now

                let x be object;

                assume

                 A12: x in (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS)));

                then

                reconsider P = x as Element of ( _bool TS);

                consider Q be Element of ( _bool TS) such that

                 A13: Q in {(v -succ_of (X,TS))} & (Q,u) ==>* (P,( _bool TS)) by A12, REWRITE3: 103;

                Q = (v -succ_of (X,TS)) & P = (u -succ_of (Q,TS)) by A8, A13, Th13, TARSKI:def 1;

                then P = ((v ^ u) -succ_of (X,TS)) by Th29;

                hence x in {((v ^ u) -succ_of (X,TS))} by TARSKI:def 1;

              end;

              hence (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ u) -succ_of (X,TS))} by A9, TARSKI: 2;

            end;

          end;

            suppose

             A14: k <> 0 ;

            reconsider bTS = ( _bool TS) as non empty transition-system over (( Lex E) \/ {( <%> E)}) by Th30;

            consider v1, v2 such that

             A15: ( len v1) <= k and

             A16: ( len v2) <= k and

             A17: u = (v1 ^ v2) by A6, A14, Th5;

            

             A18: (v1 -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ v1) -succ_of (X,TS))} by A5, A15;

            

             A19: the Tran of bTS = the Tran of ( _bool TS);

            

            then ((v1 ^ v2) -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = ((v1 ^ v2) -succ_of ( {(v -succ_of (X,TS))},bTS)) by REWRITE3: 105

            .= (v2 -succ_of ((v1 -succ_of ( {(v -succ_of (X,TS))},bTS)),bTS)) by Th29

            .= (v2 -succ_of ((v1 -succ_of ( {(v -succ_of (X,TS))},( _bool TS))),bTS)) by A19, REWRITE3: 105

            .= (v2 -succ_of ((v1 -succ_of ( {(v -succ_of (X,TS))},( _bool TS))),( _bool TS))) by A19, REWRITE3: 105

            .= {(((v ^ v1) ^ v2) -succ_of (X,TS))} by A5, A16, A18

            .= {((v ^ (v1 ^ v2)) -succ_of (X,TS))} by AFINSQ_1: 27;

            hence (u -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ u) -succ_of (X,TS))} by A17;

          end;

        end;

        hence P[(k + 1)];

      end;

      for k holds P[k] from NAT_1:sch 2( A2, A4);

      then ( len w) <= ( len w) implies (w -succ_of ( {(v -succ_of (X,TS))},( _bool TS))) = {((v ^ w) -succ_of (X,TS))};

      hence thesis;

    end;

    reserve SA for non empty semiautomaton over E, (( Lex E) \/ {( <%> E)});

    theorem :: FSM_3:32

    

     Th32: (w -succ_of ( {(( <%> E) -succ_of (X,SA))},( _bool SA))) = {(w -succ_of (X,SA))}

    proof

      set TS = the transition-system of SA;

      set Es = (( <%> E) -succ_of (X,SA));

       the transition-system of ( _bool SA) = ( _bool TS) by Def3;

      

      hence (w -succ_of ( {Es},( _bool SA))) = (w -succ_of ( {Es},( _bool TS))) by REWRITE3: 105

      .= (w -succ_of ( {(( <%> E) -succ_of (X,TS))},( _bool TS))) by REWRITE3: 105

      .= {(( {} ^ w) -succ_of (X,TS))} by Th31

      .= {(w -succ_of (X,TS))}

      .= {(w -succ_of (X,SA))} by REWRITE3: 105;

    end;

    reserve A for non empty automaton over E, (( Lex E) \/ {( <%> E)});

    reserve P for Subset of A;

    theorem :: FSM_3:33

    

     Th33: x in the FinalS of A & x in P implies P in the FinalS of ( _bool A)

    proof

      assume x in the FinalS of A & x in P;

      then

       A1: P meets the FinalS of A by XBOOLE_0: 3;

      P is Element of ( _bool A) by Th16;

      then P in { Q where Q be Element of ( _bool A) : Q meets the FinalS of A } by A1;

      hence thesis by Def6;

    end;

    theorem :: FSM_3:34

    

     Th34: X in the FinalS of ( _bool A) implies X meets the FinalS of A

    proof

      assume

       A1: X in the FinalS of ( _bool A);

      the FinalS of ( _bool A) = { Q where Q be Element of ( _bool A) : Q meets the FinalS of A } by Def6;

      then ex Q be Element of ( _bool A) st X = Q & Q meets the FinalS of A by A1;

      hence thesis;

    end;

    theorem :: FSM_3:35

    

     Th35: the InitS of ( _bool A) = {(( <%> E) -succ_of (the InitS of A,A))}

    proof

      the InitS of ( _bool A) = the InitS of the semiautomaton of ( _bool A)

      .= the InitS of ( _bool the semiautomaton of A) by Def6

      .= {(( <%> E) -succ_of (the InitS of the semiautomaton of A, the semiautomaton of A))} by Def3;

      hence thesis by REWRITE3: 105;

    end;

    theorem :: FSM_3:36

    

     Th36: (w -succ_of ( {(( <%> E) -succ_of (X,A))},( _bool A))) = {(w -succ_of (X,A))}

    proof

      set SA = the semiautomaton of A;

      set Es = (( <%> E) -succ_of (X,A));

       the semiautomaton of ( _bool A) = ( _bool SA) by Def6;

      

      hence (w -succ_of ( {Es},( _bool A))) = (w -succ_of ( {Es},( _bool SA))) by REWRITE3: 105

      .= (w -succ_of ( {(( <%> E) -succ_of (X,SA))},( _bool SA))) by REWRITE3: 105

      .= {(w -succ_of (X,SA))} by Th32

      .= {(w -succ_of (X,A))} by REWRITE3: 105;

    end;

    theorem :: FSM_3:37

    

     Th37: (w -succ_of (the InitS of ( _bool A),( _bool A))) = {(w -succ_of (the InitS of A,A))}

    proof

      set Es = (( <%> E) -succ_of (the InitS of A,A));

      the InitS of ( _bool A) = {Es} by Th35;

      hence thesis by Th36;

    end;

    theorem :: FSM_3:38

    

     Th38: ( Lang A) = ( Lang ( _bool A))

    proof

      set DA = ( _bool A);

      

       A1: w in ( Lang A) implies w in ( Lang DA)

      proof

        assume w in ( Lang A);

        then (w -succ_of (the InitS of A,A)) meets the FinalS of A by Th19;

        then ex x be object st x in (w -succ_of (the InitS of A,A)) & x in the FinalS of A by XBOOLE_0: 3;

        then

         A2: (w -succ_of (the InitS of A,A)) in the FinalS of DA by Th33;

        (w -succ_of (the InitS of DA,DA)) = {(w -succ_of (the InitS of A,A))} by Th37;

        then (w -succ_of (the InitS of A,A)) in (w -succ_of (the InitS of DA,DA)) by TARSKI:def 1;

        then (w -succ_of (the InitS of DA,DA)) meets the FinalS of DA by A2, XBOOLE_0: 3;

        hence thesis by Th19;

      end;

      w in ( Lang DA) implies w in ( Lang A)

      proof

        assume w in ( Lang DA);

        then (w -succ_of (the InitS of DA,DA)) meets the FinalS of DA by Th19;

        then

        consider x be object such that

         A3: x in (w -succ_of (the InitS of DA,DA)) and

         A4: x in the FinalS of DA by XBOOLE_0: 3;

        (w -succ_of (the InitS of ( _bool A),( _bool A))) = {(w -succ_of (the InitS of A,A))} by Th37;

        then x = (w -succ_of (the InitS of A,A)) by A3, TARSKI:def 1;

        then (w -succ_of (the InitS of A,A)) meets the FinalS of A by A4, Th34;

        hence thesis by Th19;

      end;

      hence thesis by A1, SUBSET_1: 3;

    end;

    theorem :: FSM_3:39

    for A be non empty automaton over E, (( Lex E) \/ {( <%> E)}) holds ex DA be non empty deterministic automaton over E, ( Lex E) st ( Lang A) = ( Lang DA)

    proof

      let A be non empty automaton over E, (( Lex E) \/ {( <%> E)});

      set DA = ( _bool A);

      take DA;

      thus thesis by Th38;

    end;

    theorem :: FSM_3:40

    for FA be non empty finite automaton over E, (( Lex E) \/ {( <%> E)}) holds ex DFA be non empty deterministic finite automaton over E, ( Lex E) st ( Lang FA) = ( Lang DFA)

    proof

      let FA be non empty finite automaton over E, (( Lex E) \/ {( <%> E)});

      set bNFA = ( _bool FA);

      ( Lang FA) = ( Lang bNFA) by Th38;

      hence thesis;

    end;