:: FSM_2 semantic presentation
begin
notation
let I be non empty set ;
let S be non empty FSM over I;
let q be State of S;
let w be FinSequence of I;
synonym GEN (w,q) for (q,w) -admissible ;
end;
registration
let I be non empty set ;
let S be non empty FSM over I;
let q be State of S;
let w be FinSequence of I;
cluster GEN (w,q) -> non empty ;
coherence
not GEN (w,q) is empty
proof
len (GEN (w,q)) = (len w) + 1 by FSM_1:def_2;
hence not GEN (w,q) is empty ; ::_thesis: verum
end;
end;
theorem Th1: :: FSM_2:1
for I being non empty set
for s being Element of I
for S being non empty FSM over I
for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>
proof
let I be non empty set ; ::_thesis: for s being Element of I
for S being non empty FSM over I
for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>
let s be Element of I; ::_thesis: for S being non empty FSM over I
for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>
let S be non empty FSM over I; ::_thesis: for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>
let q be State of S; ::_thesis: GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>
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 being Element of I, QI, QI1 being 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 GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> by A2, A3, A5, A6, A7, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th2: :: FSM_2:2
for I being non empty set
for s1, s2 being Element of I
for S being non empty FSM over I
for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>
proof
let I be non empty set ; ::_thesis: for s1, s2 being Element of I
for S being non empty FSM over I
for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>
let s1, s2 be Element of I; ::_thesis: for S being non empty FSM over I
for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>
let S be non empty FSM over I; ::_thesis: for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>
let q be State of S; ::_thesis: GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>
set w = <*s1,s2*>;
A1: (GEN (<*s1,s2*>,q)) . 1 = q by FSM_1:def_2;
A2: <*s1,s2*> = <*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, FSM_1:def_3;
then A4: (GEN (<*s1,s2*>,q)) . (1 + 1) = the Tran of S . [q,s1] by A2, A3, FSM_1:6;
A5: len <*s1,s2*> = 2 by FINSEQ_1:44;
2 <= len <*s1,s2*> by FINSEQ_1:44;
then consider WI being Element of I, QI, QI1 being State of S such that
A6: WI = <*s1,s2*> . 2 and
A7: QI = (GEN (<*s1,s2*>,q)) . 2 and
A8: QI1 = (GEN (<*s1,s2*>,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 (<*s1,s2*>,q)) = (len <*s1,s2*>) + 1 by FSM_1:def_2
.= 3 by A5 ;
hence GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> by A1, A4, A7, A8, A9, A10, FINSEQ_1:45; ::_thesis: verum
end;
theorem :: FSM_2:3
for I being non empty set
for s1, s2, s3 being Element of I
for S being non empty FSM over I
for q being State of S holds 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
let I be non empty set ; ::_thesis: for s1, s2, s3 being Element of I
for S being non empty FSM over I
for q being State of S holds 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])*>
let s1, s2, s3 be Element of I; ::_thesis: for S being non empty FSM over I
for q being State of S holds 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])*>
let S be non empty FSM over I; ::_thesis: for q being State of S holds 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])*>
let q be State of S; ::_thesis: 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])*>
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: <*s1,s2,s3*> = w1 ^ w2 by FINSEQ_1:43;
A2: len w1 = 2 by FINSEQ_1:44;
GEN (w1,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> by Th2;
then (GEN (w1,q)) . ((len w1) + 1) = the Tran of S . [( the Tran of S . [q,s1]),s2] by A2, FINSEQ_1:45;
then q,w1 -leads_to the Tran of S . [( the Tran of S . [q,s1]),s2] by FSM_1:def_3;
then A3: GEN (<*s1,s2,s3*>,q) = (Del ((GEN (w1,q)),((len w1) + 1))) ^ (GEN (w2,( the Tran of S . [( the Tran of S . [q,s1]),s2]))) by A1, FSM_1:8;
Del ((GEN (w1,q)),((len w1) + 1)) = Del (<*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>,3) by A2, Th2
.= <*q,( the Tran of S . [q,s1])*> by WSIERP_1:19 ;
then 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])*> by A3, Th1;
hence 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])*> by FINSEQ_4:74; ::_thesis: verum
end;
definition
let I be non empty set ;
let S be non empty FSM over I;
attrS is calculating_type means :Def1: :: FSM_2:def 1
for j being non empty Element of NAT
for w1, w2 being FinSequence of I 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;
:: deftheorem Def1 defines calculating_type FSM_2:def_1_:_
for I being non empty set
for S being non empty FSM over I holds
( S is calculating_type iff for j being non empty Element of NAT
for w1, w2 being FinSequence of I 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 );
theorem Th4: :: FSM_2:4
for I being non empty set
for S being non empty FSM over I st S is calculating_type holds
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is calculating_type holds
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
let S be non empty FSM over I; ::_thesis: ( S is calculating_type implies for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable )
assume A1: S is calculating_type ; ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable )
assume A2: w1 . 1 = w2 . 1 ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
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)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w1)) ) or ( Seg (1 + (len w2)) c= Seg (1 + (len w1)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = 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__::_thesis:_for_x_being_set_st_x_in_(Seg_(1_+_(len_w1)))_/\_(Seg_(1_+_(len_w2)))_holds_
(GEN_(w1,_the_InitS_of_S))_._x_=_(GEN_(w2,_the_InitS_of_S))_._x
let x be set ; ::_thesis: ( x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) implies (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x )
assume A8: x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) ; ::_thesis: (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x
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, Def1; ::_thesis: verum
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; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
theorem Th5: :: FSM_2:5
for I being non empty set
for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds
S is calculating_type
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds
S is calculating_type
let S be non empty FSM over I; ::_thesis: ( ( for w1, w2 being FinSequence of I 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 )
assume A1: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ; ::_thesis: S is calculating_type
let j be non empty Element of NAT ; :: according to FSM_2:def_1 ::_thesis: for w1, w2 being FinSequence of I 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
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j )
assume that
A2: w1 . 1 = w2 . 1 and
A3: j <= (len w1) + 1 and
A4: j <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
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) ) by XBOOLE_0:def_9;
then GEN (w1, the InitS of S) tolerates GEN (w2, the InitS of S) by PARTFUN1:54;
hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A9, PARTFUN1:def_4; ::_thesis: verum
end;
theorem :: FSM_2:6
for I being non empty set
for S being non empty FSM over I st S is calculating_type holds
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S)
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is calculating_type holds
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S)
let S be non empty FSM over I; ::_thesis: ( S is calculating_type implies for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S) )
assume A1: S is calculating_type ; ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S)
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN (w1, the InitS of S) = GEN (w2, the InitS of S) )
assume that
A2: w1 . 1 = w2 . 1 and
A3: len w1 = len w2 ; ::_thesis: GEN (w1, the InitS of S) = GEN (w2, the InitS of S)
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 GEN (w1, the InitS of S) = GEN (w2, the InitS of S) by A1, A2, A3, A4, Th4, TREES_1:4; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_I_being_non_empty_set_
for_S_being_non_empty_FSM_over_I
for_w_being_FinSequence_of_I
for_q_being_State_of_S_holds_GEN_((<*>_I),q),_GEN_(w,q)_are_c=-comparable
let I be non empty set ; ::_thesis: for S being non empty FSM over I
for w being FinSequence of I
for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable
let S be non empty FSM over I; ::_thesis: for w being FinSequence of I
for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable
let w be FinSequence of I; ::_thesis: for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable
let q be State of S; ::_thesis: GEN ((<*> I),q), GEN (w,q) are_c=-comparable
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 by XBOOLE_0:def_9; ::_thesis: verum
end;
Lm2: now__::_thesis:_for_p,_q_being_FinSequence_st_p_<>_{}_&_q_<>_{}_&_p_._(len_p)_=_q_._1_holds_
(Del_(p,(len_p)))_^_q_=_p_^_(Del_(q,1))
let p, q be FinSequence; ::_thesis: ( p <> {} & q <> {} & p . (len p) = q . 1 implies (Del (p,(len p))) ^ q = p ^ (Del (q,1)) )
assume that
A1: p <> {} and
A2: q <> {} and
A3: p . (len p) = q . 1 ; ::_thesis: (Del (p,(len p))) ^ q = p ^ (Del (q,1))
consider p1 being FinSequence, x being set such that
A4: p = p1 ^ <*x*> by A1, FINSEQ_1:46;
consider y being set , q1 being 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; ::_thesis: verum
end;
theorem Th7: :: FSM_2:7
for I being non empty set
for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds
S is calculating_type
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds
S is calculating_type
let S be non empty FSM over I; ::_thesis: ( ( for w1, w2 being FinSequence of I 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 )
assume A1: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ; ::_thesis: S is calculating_type
now__::_thesis:_for_w1,_w2_being_FinSequence_of_I_st_w1_._1_=_w2_._1_holds_
GEN_(w1,_the_InitS_of_S),_GEN_(w2,_the_InitS_of_S)_are_c=-comparable
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable )
assume A2: w1 . 1 = w2 . 1 ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
thus GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ::_thesis: verum
proof
percases ( w1 = <*> I or w2 = <*> I or ( w1 <> {} & w2 <> {} ) ) ;
suppose ( w1 = <*> I or w2 = <*> I ) ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
hence GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by Lm1; ::_thesis: verum
end;
supposeA3: ( w1 <> {} & w2 <> {} ) ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
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, GRAPH_2:2;
v2 . 1 = w1 . 1 by A4, A6, GRAPH_2:2;
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 being FinSequence such that
A9: w2 = v1 ^ s1 by FINSEQ_1:80;
consider s2 being FinSequence such that
A10: w1 = v2 ^ s2 by FINSEQ_1:80;
reconsider s1 = s1, s2 = s2 as FinSequence of I by A9, A10, FINSEQ_1:36;
v1 <> {}
proof
assume A11: v1 = {} ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then 1 <= len v1 by NAT_1:14;
then A13: ex WI being Element of I ex QI, QI1 being 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 = {} ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then 1 <= len v2 by NAT_1:14;
then ex WI2 being Element of I ex QI2, QI12 being 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 by FSM_1:def_3;
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 by FSM_1:def_3;
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 GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
end;
end;
end;
hence S is calculating_type by Th5; ::_thesis: verum
end;
definition
let I be non empty set ;
let S be non empty FSM over I;
let q be State of S;
let s be Element of I;
predq is_accessible_via s means :Def2: :: FSM_2:def 2
ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q;
end;
:: deftheorem Def2 defines is_accessible_via FSM_2:def_2_:_
for I being non empty set
for S being non empty FSM over I
for q being State of S
for s being Element of I holds
( q is_accessible_via s iff ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q );
definition
let I be non empty set ;
let S be non empty FSM over I;
let q be State of S;
attrq is accessible means :Def3: :: FSM_2:def 3
ex w being FinSequence of I st the InitS of S,w -leads_to q;
end;
:: deftheorem Def3 defines accessible FSM_2:def_3_:_
for I being non empty set
for S being non empty FSM over I
for q being State of S holds
( q is accessible iff ex w being FinSequence of I st the InitS of S,w -leads_to q );
theorem :: FSM_2:8
for I being non empty set
for s being Element of I
for S being non empty FSM over I
for q being State of S st q is_accessible_via s holds
q is accessible
proof
let I be non empty set ; ::_thesis: for s being Element of I
for S being non empty FSM over I
for q being State of S st q is_accessible_via s holds
q is accessible
let s be Element of I; ::_thesis: for S being non empty FSM over I
for q being State of S st q is_accessible_via s holds
q is accessible
let S be non empty FSM over I; ::_thesis: for q being State of S st q is_accessible_via s holds
q is accessible
let q be State of S; ::_thesis: ( q is_accessible_via s implies q is accessible )
assume q is_accessible_via s ; ::_thesis: q is accessible
then consider W being FinSequence of I such that
A1: the InitS of S,<*s*> ^ W -leads_to q by Def2;
take <*s*> ^ W ; :: according to FSM_2:def_3 ::_thesis: the InitS of S,<*s*> ^ W -leads_to q
thus the InitS of S,<*s*> ^ W -leads_to q by A1; ::_thesis: verum
end;
theorem :: FSM_2:9
for I being non empty set
for S being non empty FSM over I
for q being State of S st q is accessible & q <> the InitS of S holds
ex s being Element of I st q is_accessible_via s
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I
for q being State of S st q is accessible & q <> the InitS of S holds
ex s being Element of I st q is_accessible_via s
let S be non empty FSM over I; ::_thesis: for q being State of S st q is accessible & q <> the InitS of S holds
ex s being Element of I st q is_accessible_via s
let q be State of S; ::_thesis: ( q is accessible & q <> the InitS of S implies ex s being Element of I st q is_accessible_via s )
assume that
A1: q is accessible and
A2: q <> the InitS of S ; ::_thesis: ex s being Element of I st q is_accessible_via s
consider W being FinSequence of I such that
A3: the InitS of S,W -leads_to q by A1, Def3;
W <> {}
proof
assume W = {} ; ::_thesis: contradiction
then len W = 0 ;
then (GEN (W, the InitS of S)) . ((len W) + 1) = the InitS of S by FSM_1:def_2;
hence contradiction by A2, A3, FSM_1:def_3; ::_thesis: verum
end;
then consider S being Element of I, w9 being FinSequence of I such that
W . 1 = S and
A4: W = <*S*> ^ w9 by FINSEQ_3:102;
take S ; ::_thesis: q is_accessible_via S
thus q is_accessible_via S by A3, A4, Def2; ::_thesis: verum
end;
theorem :: FSM_2:10
for I being non empty set
for S being non empty FSM over I holds the InitS of S is accessible
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I holds the InitS of S is accessible
let S be non empty FSM over I; ::_thesis: the InitS of S is accessible
set w = <*> I;
(GEN ((<*> I), the InitS of S)) . ((len (<*> I)) + 1) = the InitS of S by FSM_1:def_2;
then the InitS of S, <*> I -leads_to the InitS of S by FSM_1:def_3;
hence the InitS of S is accessible by Def3; ::_thesis: verum
end;
theorem :: FSM_2:11
for I being non empty set
for s being Element of I
for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
proof
let I be non empty set ; ::_thesis: for s being Element of I
for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
let s be Element of I; ::_thesis: for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
let S be non empty FSM over I; ::_thesis: for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
let q be State of S; ::_thesis: ( S is calculating_type & q is_accessible_via s implies ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) ) )
assume A1: S is calculating_type ; ::_thesis: ( not q is_accessible_via s or ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) ) )
given w being FinSequence of I such that A2: the InitS of S,<*s*> ^ w -leads_to q ; :: according to FSM_2:def_2 ::_thesis: ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
defpred S1[ 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, FSM_1:def_3;
then A4: ex m being Nat st S1[m] by A3;
consider m being Nat such that
A5: S1[m] and
A6: for k being Nat st S1[k] holds
m <= k from NAT_1:sch_5(A4);
reconsider m = m as non empty Element of NAT by A5, ORDINAL1:def_12;
take m ; ::_thesis: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
let w1 be FinSequence of I; ::_thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies ( q = (GEN (w1, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q ) ) )
assume that
A7: (len w1) + 1 >= m and
A8: w1 . 1 = s ; ::_thesis: ( q = (GEN (w1, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q ) )
(<*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) ) by XBOOLE_0:def_9;
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; ::_thesis: for i being non empty Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q
let i be non empty Element of NAT ; ::_thesis: ( i < m implies (GEN (w1, the InitS of S)) . i <> q )
assume A13: i < m ; ::_thesis: (GEN (w1, the InitS of S)) . i <> q
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 ; ::_thesis: contradiction
then q = (GEN ((<*s*> ^ w), the InitS of S)) . i by A9, A18, A19, GRFUNC_1:2;
hence contradiction by A6, A13, A14, A15; ::_thesis: verum
end;
definition
let I be non empty set ;
let S be non empty FSM over I;
attrS is regular means :Def4: :: FSM_2:def 4
for q being State of S holds q is accessible ;
end;
:: deftheorem Def4 defines regular FSM_2:def_4_:_
for I being non empty set
for S being non empty FSM over I holds
( S is regular iff for q being State of S holds q is accessible );
theorem :: FSM_2:12
for I being non empty set
for S being non empty FSM over I st ( for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds
S is calculating_type
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds
S is calculating_type
let S be non empty FSM over I; ::_thesis: ( ( for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) implies S is calculating_type )
assume A1: for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ; ::_thesis: S is calculating_type
for j being non empty Element of NAT
for w1, w2 being FinSequence of I 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 be non empty Element of NAT ; ::_thesis: for w1, w2 being FinSequence of I 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
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j )
assume that
A2: w1 . 1 = w2 . 1 and
A3: j <= (len w1) + 1 and
A4: j <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
defpred S1[ Nat] means for w1, w2 being FinSequence of I 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: S1[1]
proof
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 )
(GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def_2;
hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def_2; ::_thesis: verum
end;
A6: for h being non empty Nat st S1[h] holds
S1[h + 1]
proof
let h be non empty Nat; ::_thesis: ( S1[h] implies S1[h + 1] )
assume A7: for w1, w2 being FinSequence of I 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 ; ::_thesis: S1[h + 1]
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & h + 1 <= (len w1) + 1 & h + 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) )
assume that
A8: w1 . 1 = w2 . 1 and
A9: h + 1 <= (len w1) + 1 and
A10: h + 1 <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 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 being Element of I, QI, QI1 being 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 being Element of I, QI2, QI12 being 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 (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A14, A15, A19, A20; ::_thesis: verum
end;
for j being non empty Nat holds S1[j] from NAT_1:sch_10(A5, A6);
hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A2, A3, A4; ::_thesis: verum
end;
hence S is calculating_type by Def1; ::_thesis: verum
end;
theorem :: FSM_2:13
for I being non empty set
for S being non empty FSM over I st ( for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I
for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds
S is calculating_type
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I
for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds
S is calculating_type
let S be non empty FSM over I; ::_thesis: ( ( for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I
for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) implies S is calculating_type )
assume that
A1: for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2] and
A2: for s being Element of I
for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ; ::_thesis: S is calculating_type
A3: for j being non empty Element of NAT st j >= 2 holds
for w1 being FinSequence of I st j <= (len w1) + 1 holds
(GEN (w1, the InitS of S)) . j <> the InitS of S
proof
let j be non empty Element of NAT ; ::_thesis: ( j >= 2 implies for w1 being FinSequence of I st j <= (len w1) + 1 holds
(GEN (w1, the InitS of S)) . j <> the InitS of S )
assume j >= 2 ; ::_thesis: for w1 being FinSequence of I st j <= (len w1) + 1 holds
(GEN (w1, the InitS of S)) . j <> the InitS of S
then j <> 1 ;
then A4: not j is trivial by NAT_2:def_1;
defpred S1[ Nat] means for w1 being FinSequence of I st $1 <= (len w1) + 1 holds
(GEN (w1, the InitS of S)) . $1 <> the InitS of S;
A5: S1[2]
proof
let w1 be FinSequence of I; ::_thesis: ( 2 <= (len w1) + 1 implies (GEN (w1, the InitS of S)) . 2 <> the InitS of S )
assume 2 <= (len w1) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . 2 <> the InitS of S
then 1 + 1 <= (len w1) + 1 ;
then 1 <= len w1 by XREAL_1:6;
then ex WI being Element of I ex QI, QI1 being 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 (GEN (w1, the InitS of S)) . 2 <> the InitS of S by A2; ::_thesis: verum
end;
A6: for h being non trivial Nat st S1[h] holds
S1[h + 1]
proof
let h be non trivial Nat; ::_thesis: ( S1[h] implies S1[h + 1] )
assume for w1 being FinSequence of I st h <= (len w1) + 1 holds
(GEN (w1, the InitS of S)) . h <> the InitS of S ; ::_thesis: S1[h + 1]
let w1 be FinSequence of I; ::_thesis: ( h + 1 <= (len w1) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S )
assume A7: h + 1 <= (len w1) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S
A8: 1 <= h by NAT_1:14;
h <= len w1 by A7, XREAL_1:6;
then ex WI being Element of I ex QI, QI1 being 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 (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S by A2; ::_thesis: verum
end;
for h being non trivial Nat holds S1[h] from NAT_2:sch_2(A5, A6);
hence for w1 being FinSequence of I st j <= (len w1) + 1 holds
(GEN (w1, the InitS of S)) . j <> the InitS of S by A4; ::_thesis: verum
end;
for j being non empty Element of NAT
for w1, w2 being FinSequence of I 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 be non empty Element of NAT ; ::_thesis: for w1, w2 being FinSequence of I 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
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j )
assume that
A9: w1 . 1 = w2 . 1 and
A10: j <= (len w1) + 1 and
A11: j <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
defpred S1[ Nat] means for w1, w2 being FinSequence of I 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: S1[1]
proof
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 )
(GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def_2;
hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def_2; ::_thesis: verum
end;
A13: for h being non empty Nat st S1[h] holds
S1[h + 1]
proof
let h be non empty Nat; ::_thesis: ( S1[h] implies S1[h + 1] )
assume A14: for w1, w2 being FinSequence of I 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 ; ::_thesis: S1[h + 1]
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & h + 1 <= (len w1) + 1 & h + 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) )
assume that
A15: w1 . 1 = w2 . 1 and
A16: h + 1 <= (len w1) + 1 and
A17: h + 1 <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 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 being Element of I, QI, QI1 being 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 being Element of I, QI2, QI12 being 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 (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A3, A15, A19, A21, A22, A23, A24, A27, A29, A30, A31, A32; ::_thesis: verum
end;
for j being non empty Nat holds S1[j] from NAT_1:sch_10(A12, A13);
hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A9, A10, A11; ::_thesis: verum
end;
hence S is calculating_type by Def1; ::_thesis: verum
end;
theorem Th14: :: FSM_2:14
for I being non empty set
for S being non empty FSM over I st S is regular & S is calculating_type holds
for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds
for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
let S be non empty FSM over I; ::_thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 )
assume that
A1: S is regular and
A2: S is calculating_type ; ::_thesis: for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
let s1, s2 be Element of I; ::_thesis: for q being State of S st q <> the InitS of S holds
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
let q be State of S; ::_thesis: ( q <> the InitS of S implies (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 )
assume A3: q <> the InitS of S ; ::_thesis: (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
q is accessible by A1, Def4;
then consider w being FinSequence of I such that
A4: the InitS of S,w -leads_to q by Def3;
w <> {}
proof
assume w = {} ; ::_thesis: contradiction
then len w = 0 ;
then (GEN (w, the InitS of S)) . ((len w) + 1) = the InitS of S by FSM_1:def_2;
hence contradiction by A3, A4, FSM_1:def_3; ::_thesis: verum
end;
then consider x being Element of I, w9 being FinSequence of I such that
w . 1 = x and
A5: w = <*x*> ^ w9 by FINSEQ_3:102;
set w1 = w ^ <*s1*>;
set 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 = (w ^ <*s1*>) . 1 by FINSEQ_1:def_7;
then A7: (w ^ <*s1*>) . 1 = (w ^ <*s2*>) . 1 by A6, FINSEQ_1:def_7;
A8: len <*s1*> = 1 by FINSEQ_1:39;
then A9: len (w ^ <*s1*>) = (len w) + 1 by FINSEQ_1:22;
A10: len <*s2*> = 1 by FINSEQ_1:39;
then A11: len (w ^ <*s2*>) = (len w) + 1 by FINSEQ_1:22;
A12: len (w ^ <*s1*>) = len (w ^ <*s2*>) 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 ((w ^ <*s1*>), the InitS of S) = (Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q)) by A4, FSM_1:8;
A14: len (GEN (w, the InitS of S)) = (len w) + 1 by FSM_1:def_2;
then A15: len (Del ((GEN (w, the InitS of S)),((len w) + 1))) = len w by PRE_POLY:12;
A16: len (GEN (<*s1*>,q)) = (len <*s1*>) + 1 by FSM_1:def_2
.= 1 + 1 by FINSEQ_1:39 ;
A17: len (GEN ((w ^ <*s1*>), the InitS of S)) = len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q))) by A4, FSM_1:8
.= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s1*>,q))) by FINSEQ_1:22
.= (len w) + (1 + 1) by A14, A16, PRE_POLY:12
.= ((len w) + 1) + 1
.= (len (w ^ <*s1*>)) + 1 by A8, FINSEQ_1:22 ;
A18: (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + 1 <= (len (w ^ <*s1*>)) + 1 by A9, A15, NAT_1:11;
len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q))) = (len (w ^ <*s1*>)) + 1 by A4, A17, FSM_1:8;
then (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s1*>,q))) = (len (w ^ <*s1*>)) + 1 by FINSEQ_1:22;
then A19: (GEN ((w ^ <*s1*>), the InitS of S)) . ((len (w ^ <*s1*>)) + 1) = (GEN (<*s1*>,q)) . (((len (w ^ <*s1*>)) + 1) - (len (Del ((GEN (w, the InitS of S)),((len w) + 1))))) by A13, A18, FINSEQ_1:23
.= (GEN (<*s1*>,q)) . (((len (w ^ <*s1*>)) + 1) - (len w)) by A14, PRE_POLY:12
.= (GEN (<*s1*>,q)) . ((((len w) + 1) + 1) - (len w)) by A8, FINSEQ_1:22
.= (GEN (<*s1*>,q)) . 2 ;
set p2 = GEN (<*s2*>,q);
A20: GEN ((w ^ <*s2*>), the InitS of S) = (Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q)) by A4, FSM_1:8;
A21: len (GEN (<*s2*>,q)) = (len <*s2*>) + 1 by FSM_1:def_2
.= 1 + 1 by FINSEQ_1:39 ;
A22: len (GEN ((w ^ <*s2*>), the InitS of S)) = len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q))) by A4, FSM_1:8
.= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s2*>,q))) by FINSEQ_1:22
.= (len w) + (1 + 1) by A14, A21, PRE_POLY:12
.= ((len w) + 1) + 1
.= (len (w ^ <*s2*>)) + 1 by A10, FINSEQ_1:22 ;
(len w) + 1 <= (len (w ^ <*s2*>)) + 1 by A11, NAT_1:11;
then A23: (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + 1 <= (len (w ^ <*s2*>)) + 1 by A14, PRE_POLY:12;
len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q))) = (len (w ^ <*s2*>)) + 1 by A4, A22, FSM_1:8;
then (len (w ^ <*s2*>)) + 1 <= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s2*>,q))) by FINSEQ_1:22;
then (GEN ((w ^ <*s2*>), the InitS of S)) . ((len (w ^ <*s2*>)) + 1) = (GEN (<*s2*>,q)) . (((len (w ^ <*s2*>)) + 1) - (len (Del ((GEN (w, the InitS of S)),((len w) + 1))))) by A20, A23, FINSEQ_1:23
.= (GEN (<*s2*>,q)) . (((len (w ^ <*s2*>)) + 1) - (len w)) by A14, PRE_POLY:12
.= (GEN (<*s2*>,q)) . ((((len w) + 1) + 1) - (len w)) by A10, FINSEQ_1:22
.= (GEN (<*s2*>,q)) . 2 ;
hence (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 by A2, A7, A12, A19, Def1; ::_thesis: verum
end;
theorem :: FSM_2:15
for I being non empty set
for S being non empty FSM over I st S is regular & S is calculating_type holds
for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
proof
let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds
for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
let S be non empty FSM over I; ::_thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2] )
assume that
A1: S is regular and
A2: S is calculating_type ; ::_thesis: for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
let s1, s2 be Element of I; ::_thesis: for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
let q be State of S; ::_thesis: ( q <> the InitS of S implies the Tran of S . [q,s1] = the Tran of S . [q,s2] )
assume A3: q <> the InitS of S ; ::_thesis: the Tran of S . [q,s1] = the Tran of S . [q,s2]
set w1 = <*s1*>;
set w2 = <*s2*>;
A4: len <*s1*> = 0 + 1 by FINSEQ_1:39;
reconsider j = len <*s1*> as non empty Element of NAT ;
consider WI being Element of I, QI, QI1 being State of S such that
A5: WI = <*s1*> . j and
A6: QI = (GEN (<*s1*>,q)) . j and
A7: QI1 = (GEN (<*s1*>,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 <*s2*> = 0 + 1 by FINSEQ_1:39;
reconsider h = len <*s2*> as non empty Element of NAT ;
consider WI2 being Element of I, QI2, QI12 being State of S such that
A11: WI2 = <*s2*> . h and
A12: QI2 = (GEN (<*s2*>,q)) . h and
A13: QI12 = (GEN (<*s2*>,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 the Tran of S . [q,s1] = the Tran of S . [q,s2] by A1, A2, A3, A4, A7, A9, A10, A13, A14, A15, Th14; ::_thesis: verum
end;
theorem :: FSM_2:16
for I being non empty set
for S being non empty FSM over I st S is regular & S is calculating_type holds
for s, s1, s2 being Element of I
for q being State of S 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
let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds
for s, s1, s2 being Element of I
for q being State of S 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
let S be non empty FSM over I; ::_thesis: ( S is regular & S is calculating_type implies for s, s1, s2 being Element of I
for q being State of S 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 )
assume that
A1: S is regular and
A2: S is calculating_type ; ::_thesis: for s, s1, s2 being Element of I
for q being State of S 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
let s, s1, s2 be Element of I; ::_thesis: for q being State of S 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
let q be State of S; ::_thesis: ( the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] implies the Tran of S . [q,s] <> the InitS of S )
assume A3: the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] ; ::_thesis: the Tran of S . [q,s] <> the InitS of S
q is accessible by A1, Def4;
then consider w being FinSequence of I such that
A4: the InitS of S,w -leads_to q by Def3;
A5: (GEN (w, the InitS of S)) . ((len w) + 1) = q by A4, FSM_1:def_3;
assume A6: the Tran of S . [q,s] = the InitS of S ; ::_thesis: contradiction
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;
percases ( w = {} or w <> {} ) ;
suppose w = {} ; ::_thesis: contradiction
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, Def1; ::_thesis: verum
end;
suppose w <> {} ; ::_thesis: contradiction
then consider s9 being set , w9 being 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, Def1; ::_thesis: verum
end;
end;
end;
begin
definition
let I be set ;
attrc2 is strict ;
struct SM_Final over I -> FSM over I;
aggrSM_Final(# carrier, Tran, InitS, FinalS #) -> SM_Final over I;
sel FinalS c2 -> Subset of the carrier of c2;
end;
registration
let I be set ;
cluster non empty for SM_Final over I;
existence
not for b1 being SM_Final over I holds b1 is empty
proof
set A = the non empty set ;
set T = the Function of [: the non empty set ,I:], the non empty set ;
set I = the Element of the non empty set ;
set F = the Subset of the non empty set ;
take S = SM_Final(# the non empty set , the Function of [: the non empty set ,I:], the non empty set , the Element of the non empty set , the Subset of the non empty set #); ::_thesis: not S is empty
thus not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
definition
let I be non empty set ;
let s be Element of I;
let S be non empty SM_Final over I;
preds leads_to_final_state_of S means :Def5: :: FSM_2:def 5
ex q being State of S st
( q is_accessible_via s & q in the FinalS of S );
end;
:: deftheorem Def5 defines leads_to_final_state_of FSM_2:def_5_:_
for I being non empty set
for s being Element of I
for S being non empty SM_Final over I holds
( s leads_to_final_state_of S iff ex q being State of S st
( q is_accessible_via s & q in the FinalS of S ) );
definition
let I be non empty set ;
let S be non empty SM_Final over I;
attrS is halting means :Def6: :: FSM_2:def 6
for s being Element of I holds s leads_to_final_state_of S;
end;
:: deftheorem Def6 defines halting FSM_2:def_6_:_
for I being non empty set
for S being non empty SM_Final over I holds
( S is halting iff for s being Element of I holds s leads_to_final_state_of S );
definition
let I be set ;
let O be non empty set ;
attrc3 is strict ;
struct Moore-SM_Final over I,O -> SM_Final over I, Moore-FSM over I,O;
aggrMoore-SM_Final(# carrier, Tran, OFun, InitS, FinalS #) -> Moore-SM_Final over I,O;
end;
registration
let I be set ;
let O be non empty set ;
cluster non empty strict for Moore-SM_Final over I,O;
existence
ex b1 being Moore-SM_Final over I,O st
( not b1 is empty & b1 is strict )
proof
set A = the non empty set ;
set T = the Function of [: the non empty set ,I:], the non empty set ;
set o = the Function of the non empty set ,O;
set I = the Element of the non empty set ;
set F = the Subset of the non empty set ;
take S = Moore-SM_Final(# the non empty set , the Function of [: the non empty set ,I:], the non empty set , the Function of the non empty set ,O, the Element of the non empty set , the Subset of the non empty set #); ::_thesis: ( not S is empty & S is strict )
thus not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is strict
thus S is strict ; ::_thesis: verum
end;
end;
definition
let I, O be non empty set ;
let i, f be set ;
let o be Function of {i,f},O;
funcI -TwoStatesMooreSM (i,f,o) -> non empty strict Moore-SM_Final over I,O means :Def7: :: FSM_2:def 7
( the carrier of it = {i,f} & the Tran of it = [:{i,f},I:] --> f & the OFun of it = o & the InitS of it = i & the FinalS of it = {f} );
uniqueness
for b1, b2 being non empty strict Moore-SM_Final over I,O st the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} & the carrier of b2 = {i,f} & the Tran of b2 = [:{i,f},I:] --> f & the OFun of b2 = o & the InitS of b2 = i & the FinalS of b2 = {f} holds
b1 = b2 ;
existence
ex b1 being non empty strict Moore-SM_Final over I,O st
( the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} )
proof
set X = {i,f};
reconsider ii = i, ff = f as Element of {i,f} by TARSKI:def_2;
reconsider oo = o as Function of {i,f},O ;
not Moore-SM_Final(# {i,f},([:{i,f},I:] --> ff),oo,ii,{ff} #) is empty ;
hence ex b1 being non empty strict Moore-SM_Final over I,O st
( the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} ) ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines -TwoStatesMooreSM FSM_2:def_7_:_
for I, O being non empty set
for i, f being set
for o being Function of {i,f},O
for b6 being non empty strict Moore-SM_Final over I,O holds
( b6 = I -TwoStatesMooreSM (i,f,o) iff ( the carrier of b6 = {i,f} & the Tran of b6 = [:{i,f},I:] --> f & the OFun of b6 = o & the InitS of b6 = i & the FinalS of b6 = {f} ) );
theorem Th17: :: FSM_2:17
for O, I being non empty set
for w being FinSequence of I
for i, f being set
for o being Function of {i,f},O
for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
proof
let O, I be non empty set ; ::_thesis: for w being FinSequence of I
for i, f being set
for o being Function of {i,f},O
for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let w be FinSequence of I; ::_thesis: for i, f being set
for o being Function of {i,f},O
for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let i, f be set ; ::_thesis: for o being Function of {i,f},O
for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let o be Function of {i,f},O; ::_thesis: for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let j be non empty Element of NAT ; ::_thesis: ( 1 < j & j <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f )
assume A1: 1 < j ; ::_thesis: ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f )
set M = I -TwoStatesMooreSM (i,f,o);
A2: the carrier of (I -TwoStatesMooreSM (i,f,o)) = {i,f} by Def7;
A3: the Tran of (I -TwoStatesMooreSM (i,f,o)) = [:{i,f},I:] --> f by Def7;
defpred S1[ Nat] means ( $1 <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . $1 = f );
A4: S1[2]
proof
assume 2 <= (len w) + 1 ; ::_thesis: (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 2 = f
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 being Element of I ex QI, QI1 being State of (I -TwoStatesMooreSM (i,f,o)) st
( WI = w . 1 & QI = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 1 & QI1 = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (1 + 1) & WI -succ_of QI = QI1 ) by FSM_1:def_2;
hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 2 = f by A2, A3, FUNCOP_1:7; ::_thesis: verum
end;
A5: for k being non trivial Nat st S1[k] holds
S1[k + 1]
proof
let k be non trivial Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
( k <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . k = f ) and
A6: k + 1 <= (len w) + 1 ; ::_thesis: (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f
A7: 1 <= k by NAT_2:19;
k <= len w by A6, XREAL_1:6;
then ex WI being Element of I ex QI, QI1 being State of (I -TwoStatesMooreSM (i,f,o)) st
( WI = w . k & QI = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . k & QI1 = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) & WI -succ_of QI = QI1 ) by A7, FSM_1:def_2;
hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f by A2, A3, FUNCOP_1:7; ::_thesis: verum
end;
A8: j is non trivial Nat by A1, NAT_2:def_1;
for k being non trivial Nat holds S1[k] from NAT_2:sch_2(A4, A5);
hence ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f ) by A8; ::_thesis: verum
end;
registration
let I, O be non empty set ;
let i, f be set ;
let o be Function of {i,f},O;
clusterI -TwoStatesMooreSM (i,f,o) -> non empty calculating_type strict ;
coherence
I -TwoStatesMooreSM (i,f,o) is calculating_type
proof
set M = I -TwoStatesMooreSM (i,f,o);
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o)))
proof
let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) )
assume that
w1 . 1 = w2 . 1 and
A1: len w1 = len w2 ; ::_thesis: GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o)))
reconsider p = GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))), q = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) as FinSequence ;
A2: p . 1 = the InitS of (I -TwoStatesMooreSM (i,f,o)) 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__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_p_holds_
p_._j_=_q_._j
let j be Nat; ::_thesis: ( 1 <= j & j <= len p implies p . j = q . j )
assume A5: 1 <= j ; ::_thesis: ( j <= len p implies p . j = q . j )
A6: j in NAT by ORDINAL1:def_12;
( j = 1 or j > 1 ) by A5, XXREAL_0:1;
then not ( not p . j = q . j & j <= len p & not ( p . j = f & q . j = f ) ) by A1, A2, A3, A6, Th17;
hence ( j <= len p implies p . j = q . j ) ; ::_thesis: verum
end;
hence GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) by A3, A4, FINSEQ_1:14; ::_thesis: verum
end;
hence I -TwoStatesMooreSM (i,f,o) is calculating_type by Th7; ::_thesis: verum
end;
end;
registration
let I, O be non empty set ;
let i, f be set ;
let o be Function of {i,f},O;
clusterI -TwoStatesMooreSM (i,f,o) -> non empty halting strict ;
coherence
I -TwoStatesMooreSM (i,f,o) is halting
proof
let s be Element of I; :: according to FSM_2:def_6 ::_thesis: s leads_to_final_state_of I -TwoStatesMooreSM (i,f,o)
{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 ; :: according to FSM_2:def_5 ::_thesis: ( q is_accessible_via s & q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) )
thus q is_accessible_via s ::_thesis: q in the FinalS of (I -TwoStatesMooreSM (i,f,o))
proof
take w = <*> I; :: according to FSM_2:def_2 ::_thesis: the InitS of (I -TwoStatesMooreSM (i,f,o)),<*s*> ^ w -leads_to q
<*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; :: according to FSM_1:def_3 ::_thesis: verum
end;
the FinalS of (I -TwoStatesMooreSM (i,f,o)) = {f} by Def7;
hence q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def_1; ::_thesis: verum
end;
end;
theorem Th18: :: FSM_2:18
for O, I being non empty set
for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex m being non empty Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT 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
let O, I be non empty set ; ::_thesis: for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex m being non empty Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex m being non empty Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
let M be non empty Moore-SM_Final over I,O; ::_thesis: ( M is calculating_type & s leads_to_final_state_of M implies ex m being non empty Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) )
assume A1: M is calculating_type ; ::_thesis: ( not s leads_to_final_state_of M or ex m being non empty Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) )
given q being State of M such that A2: q is_accessible_via s and
A3: q in the FinalS of M ; :: according to FSM_2:def_5 ::_thesis: ex m being non empty Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
consider w being FinSequence of I such that
A4: the InitS of M,<*s*> ^ w -leads_to q by A2, Def2;
defpred S1[ 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, FSM_1:def_3;
then A6: ex m being Nat st S1[m] by A3, A5;
consider m being Nat such that
A7: S1[m] and
A8: for k being Nat st S1[k] holds
m <= k from NAT_1:sch_5(A6);
reconsider m = m as non empty Element of NAT by A7, ORDINAL1:def_12;
take m ; ::_thesis: ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
hereby ::_thesis: for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M
let w1 be FinSequence of I; ::_thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies (GEN (w1, the InitS of M)) . m in the FinalS of M )
assume that
A9: (len w1) + 1 >= m and
A10: w1 . 1 = s ; ::_thesis: (GEN (w1, the InitS of M)) . m in the FinalS of 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, 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) ) by XBOOLE_0:def_9;
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; ::_thesis: verum
end;
let w1 be FinSequence of I; ::_thesis: for j being non empty Element of NAT st j <= (len w1) + 1 & w1 . 1 = s & j < m holds
not (GEN (w1, the InitS of M)) . j in the FinalS of M
let i be non empty Element of NAT ; ::_thesis: ( i <= (len w1) + 1 & w1 . 1 = s & i < m implies not (GEN (w1, the InitS of M)) . i in the FinalS of M )
assume that
A15: i <= (len w1) + 1 and
A16: w1 . 1 = s and
A17: i < m ; ::_thesis: not (GEN (w1, the InitS of M)) . i in the FinalS of 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) ) by XBOOLE_0:def_9;
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 ; ::_thesis: contradiction
then (GEN ((<*s*> ^ w), the InitS of M)) . i in the FinalS of M by A18, A22, A23, GRFUNC_1:2;
hence contradiction by A8, A17, A19, A20; ::_thesis: verum
end;
begin
definition
let I, O be non empty set ;
let M be non empty Moore-SM_Final over I,O;
let s be Element of I;
let t be set ;
predt is_result_of s,M means :Def8: :: FSM_2:def 8
ex m being non empty Element of NAT st
for w being FinSequence of I 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 being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) );
end;
:: deftheorem Def8 defines is_result_of FSM_2:def_8_:_
for I, O being non empty set
for M being non empty Moore-SM_Final over I,O
for s being Element of I
for t being set holds
( t is_result_of s,M iff ex m being non empty Element of NAT st
for w being FinSequence of I 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 being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) );
theorem :: FSM_2:19
for I, O being non empty set
for s being Element of I
for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds
the OFun of M . the InitS of M is_result_of s,M
proof
let I, O be non empty set ; ::_thesis: for s being Element of I
for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds
the OFun of M . the InitS of M is_result_of s,M
let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds
the OFun of M . the InitS of M is_result_of s,M
let M be non empty Moore-SM_Final over I,O; ::_thesis: ( the InitS of M in the FinalS of M implies the OFun of M . the InitS of M is_result_of s,M )
assume A1: the InitS of M in the FinalS of M ; ::_thesis: the OFun of M . the InitS of M is_result_of s,M
take 1 ; :: according to FSM_2:def_8 ::_thesis: for w being FinSequence of I st w . 1 = s holds
( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) )
let w be FinSequence of I; ::_thesis: ( w . 1 = s implies ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) )
assume w . 1 = s ; ::_thesis: ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) )
thus ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) by A1, FSM_1:def_2, NAT_1:14; ::_thesis: verum
end;
theorem Th20: :: FSM_2:20
for I, O being non empty set
for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex t being Element of O st t is_result_of s,M
proof
let I, O be non empty set ; ::_thesis: for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex t being Element of O st t is_result_of s,M
let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex t being Element of O st t is_result_of s,M
let M be non empty Moore-SM_Final over I,O; ::_thesis: ( M is calculating_type & s leads_to_final_state_of M implies ex t being Element of O st t is_result_of s,M )
assume that
A1: M is calculating_type and
A2: s leads_to_final_state_of M ; ::_thesis: ex t being Element of O st t is_result_of s,M
consider q being State of M such that
A3: q is_accessible_via s and
A4: q in the FinalS of M by A2, Def5;
consider w being FinSequence of I such that
A5: the InitS of M,<*s*> ^ w -leads_to q by A3, Def2;
A6: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A5, FSM_1:def_3;
consider m being non empty Element of NAT such that
A7: for w being FinSequence of I 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 being FinSequence of I
for j being non empty Element of NAT 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 ; ::_thesis: t is_result_of s,M
take m ; :: according to FSM_2:def_8 ::_thesis: for w being FinSequence of I 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 being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) )
let w1 be FinSequence of I; ::_thesis: ( w1 . 1 = s implies ( ( 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 ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds
not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) )
assume A11: w1 . 1 = s ; ::_thesis: ( ( 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 ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds
not (GEN (w1, the InitS of M)) . n in the FinalS of M ) )
(<*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, Def1; ::_thesis: for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds
not (GEN (w1, the InitS of M)) . n in the FinalS of M
thus for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds
not (GEN (w1, the InitS of M)) . n in the FinalS of M by A8, A11; ::_thesis: verum
end;
theorem Th21: :: FSM_2:21
for I, O being non empty set
for s being Element of I
for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds
for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
proof
let I, O be non empty set ; ::_thesis: for s being Element of I
for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds
for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds
for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
let M be non empty Moore-SM_Final over I,O; ::_thesis: ( s leads_to_final_state_of M implies for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2 )
assume A1: s leads_to_final_state_of M ; ::_thesis: for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
let t1, t2 be Element of O; ::_thesis: ( t1 is_result_of s,M & t2 is_result_of s,M implies t1 = t2 )
given m being non empty Element of NAT such that A2: for w1 being FinSequence of I 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 being non empty Element of NAT st n < m & n <= (len w1) + 1 holds
not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) ; :: according to FSM_2:def_8 ::_thesis: ( not t2 is_result_of s,M or t1 = t2 )
given o being non empty Element of NAT such that A3: for w2 being FinSequence of I 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 being non empty Element of NAT st p < o & p <= (len w2) + 1 holds
not (GEN (w2, the InitS of M)) . p in the FinalS of M ) ) ; :: according to FSM_2:def_8 ::_thesis: t1 = t2
consider q being State of M such that
A4: q is_accessible_via s and
A5: q in the FinalS of M by A1, Def5;
consider w being FinSequence of I such that
A6: the InitS of M,<*s*> ^ w -leads_to q by A4, Def2;
set w1 = <*s*> ^ w;
A7: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A6, FSM_1:def_3;
A8: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;
then A9: (len (<*s*> ^ w)) + 1 >= m by A2, A5, A7;
A10: o <= (len (<*s*> ^ w)) + 1 by A3, A5, A7, A8;
A11: ( o < m or o = m or o > m ) by XXREAL_0:1;
A12: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;
then A13: t1 = the OFun of M . ((GEN ((<*s*> ^ w), the InitS of M)) . m) by A2, A9;
A14: (GEN ((<*s*> ^ w), the InitS of M)) . m in the FinalS of M by A2, A9, A12;
(GEN ((<*s*> ^ w), the InitS of M)) . o in the FinalS of M by A3, A10, A12;
hence t1 = t2 by A2, A3, A9, A10, A11, A12, A13, A14; ::_thesis: verum
end;
theorem Th22: :: FSM_2:22
for X being non empty set
for f being BinOp of X
for M being non empty Moore-SM_Final over [:X,X:], succ X st M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & ( for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ) holds
( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )
proof
let X be non empty set ; ::_thesis: for f being BinOp of X
for M being non empty Moore-SM_Final over [:X,X:], succ X st M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & ( for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ) holds
( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )
let f be BinOp of X; ::_thesis: for M being non empty Moore-SM_Final over [:X,X:], succ X st M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & ( for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ) holds
( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )
let M be non empty Moore-SM_Final over [:X,X:], succ X; ::_thesis: ( M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & ( for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ) implies ( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) ) )
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 being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ; ::_thesis: ( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )
A7: not the InitS of M in the FinalS of M by A3, A4;
hereby :: according to FSM_2:def_6 ::_thesis: for x, y being Element of X holds f . (x,y) is_result_of [x,y],M
let s be Element of [:X,X:]; ::_thesis: s leads_to_final_state_of M
consider x, y being set such that
A9: x in X and
A10: y in X and
A11: s = [x,y] by ZFMISC_1:def_2;
reconsider x = x, y = y as Element of X by A9, A10;
thus s leads_to_final_state_of M ::_thesis: verum
proof
reconsider q = f . (x,y) as State of M by A2, XBOOLE_0:def_3;
take q ; :: according to FSM_2:def_5 ::_thesis: ( q is_accessible_via s & q in the FinalS of M )
thus q is_accessible_via s ::_thesis: q in the FinalS of M
proof
take w = <*> [:X,X:]; :: according to FSM_2:def_2 ::_thesis: the InitS of M,<*s*> ^ w -leads_to q
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 being Element of [:X,X:] ex QI, QI1 being 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 the InitS of M,<*s*> ^ w -leads_to q by FSM_1:def_3; ::_thesis: verum
end;
thus q in the FinalS of M by A3; ::_thesis: verum
end;
end;
let x, y be Element of X; ::_thesis: f . (x,y) is_result_of [x,y],M
consider m being non empty Element of NAT such that
A14: for w being 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 being FinSequence of [:X,X:]
for i being non empty 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 ; :: according to FSM_2:def_8 ::_thesis: for w being FinSequence of [:X,X:] st w . 1 = [x,y] holds
( ( m <= (len w) + 1 implies ( f . (x,y) = 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 being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) )
set s = [x,y];
set t = f . (x,y);
let w be FinSequence of [:X,X:]; ::_thesis: ( w . 1 = [x,y] implies ( ( m <= (len w) + 1 implies ( f . (x,y) = 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 being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) )
assume A16: w . 1 = [x,y] ; ::_thesis: ( ( m <= (len w) + 1 implies ( f . (x,y) = 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 being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) )
hereby ::_thesis: for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M
assume A17: m <= (len w) + 1 ; ::_thesis: ( f . (x,y) = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M )
(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 being Element of [:X,X:] ex QI, QI1 being 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 f . (x,y) = the OFun of M . ((GEN (w, the InitS of M)) . m) by A2, A3, A5, A15, A16, A20, A21, A22, FUNCT_1:18; ::_thesis: (GEN (w, the InitS of M)) . m in the FinalS of M
thus (GEN (w, the InitS of M)) . m in the FinalS of M by A14, A16, A17; ::_thesis: verum
end;
thus for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M by A15, A16; ::_thesis: verum
end;
theorem Th23: :: FSM_2:23
for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) holds
for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M
proof
consider f being BinOp of REAL such that
A1: for x, y being Real holds f . (x,y) = max (x,y) from BINOP_1:sch_4();
let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )
assume that
A2: M is calculating_type and
A3: the carrier of M = succ REAL and
A4: the FinalS of M = REAL and
A5: the InitS of M = REAL and
A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st
( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st
( x < y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )
assume that
A7: for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x and
A8: for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M
let x, y be Real; ::_thesis: max (x,y) is_result_of [x,y],M
now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y)
let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
A9: ( x >= y implies the Tran of M . [ the InitS of M,[x,y]] = x ) by A7;
( x < y implies the Tran of M . [ the InitS of M,[x,y]] = y ) by A8;
then the Tran of M . [ the InitS of M,[x,y]] = max (x,y) by A9, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum
end;
then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22;
hence max (x,y) is_result_of [x,y],M by A1; ::_thesis: verum
end;
theorem Th24: :: FSM_2:24
for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) holds
for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M
proof
consider f being BinOp of REAL such that
A1: for x, y being Real holds f . (x,y) = min (x,y) from BINOP_1:sch_4();
let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M )
assume that
A2: M is calculating_type and
A3: the carrier of M = succ REAL and
A4: the FinalS of M = REAL and
A5: the InitS of M = REAL and
A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st
( x < y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st
( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M )
assume that
A7: for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = x and
A8: for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M
let x, y be Real; ::_thesis: min (x,y) is_result_of [x,y],M
now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y)
let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
A9: ( x < y implies the Tran of M . [ the InitS of M,[x,y]] = x ) by A7;
( x >= y implies the Tran of M . [ the InitS of M,[x,y]] = y ) by A8;
then the Tran of M . [ the InitS of M,[x,y]] = min (x,y) by A9, XXREAL_0:def_9;
hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum
end;
then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22;
hence min (x,y) is_result_of [x,y],M by A1; ::_thesis: verum
end;
theorem Th25: :: FSM_2:25
for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) holds
for x, y being Element of REAL holds x + y is_result_of [x,y],M
proof
deffunc H1( Real, Real) -> Element of REAL = $1 + $2;
consider f being BinOp of REAL such that
A1: for x, y being Real holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) implies for x, y being Element of REAL holds x + y is_result_of [x,y],M )
assume that
A2: M is calculating_type and
A3: the carrier of M = succ REAL and
A4: the FinalS of M = REAL and
A5: the InitS of M = REAL and
A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st not the Tran of M . [ the InitS of M,[x,y]] = x + y or for x, y being Element of REAL holds x + y is_result_of [x,y],M )
assume A7: for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ; ::_thesis: for x, y being Element of REAL holds x + y is_result_of [x,y],M
let x, y be Real; ::_thesis: x + y is_result_of [x,y],M
now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y)
let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
the Tran of M . [ the InitS of M,[x,y]] = x + y by A7;
hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum
end;
then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22;
hence x + y is_result_of [x,y],M by A1; ::_thesis: verum
end;
theorem Th26: :: FSM_2:26
for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real 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 being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds
for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M
proof
deffunc H1( Real, Real) -> Element of REAL = max ((sgn $1),(sgn $2));
consider f being BinOp of REAL such that
A1: for x, y being Real holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real 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 being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )
assume that
A2: M is calculating_type and
A3: the carrier of M = succ REAL and
A4: the FinalS of M = REAL and
A5: the InitS of M = REAL and
A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st
( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st
( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st
( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )
assume that
A7: for x, y being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 and
A8: for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds
the Tran of M . [ the InitS of M,[x,y]] = 0 and
A9: for x, y being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ; ::_thesis: for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M
let x, y be Real; ::_thesis: max ((sgn x),(sgn y)) is_result_of [x,y],M
now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y)
let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
proof
now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y))
percases ( x > 0 or x = 0 or x < 0 ) ;
supposeA10: x > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then A11: sgn x = 1 by ABSVALUE:def_2;
now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y))
percases ( y > 0 or y = 0 or y < 0 ) ;
suppose y > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = 1 by ABSVALUE:def_2;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10, A11; ::_thesis: verum
end;
suppose y = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = 0 by ABSVALUE:def_2;
then max ((sgn x),(sgn y)) = 1 by A11, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10; ::_thesis: verum
end;
suppose y < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = - 1 by ABSVALUE:def_2;
then max ((sgn x),(sgn y)) = 1 by A11, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10; ::_thesis: verum
end;
end;
end;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum
end;
supposeA12: x = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then A13: sgn x = 0 by ABSVALUE:def_2;
now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y))
percases ( y > 0 or y = 0 or y < 0 ) ;
supposeA14: y > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = 1 by ABSVALUE:def_2;
then max ((sgn x),(sgn y)) = 1 by A13, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A14; ::_thesis: verum
end;
supposeA15: y = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = 0 by ABSVALUE:def_2;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A12, A15; ::_thesis: verum
end;
supposeA16: y < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = - 1 by ABSVALUE:def_2;
then max ((sgn x),(sgn y)) = 0 by A13, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A12, A16; ::_thesis: verum
end;
end;
end;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum
end;
supposeA17: x < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then A18: sgn x = - 1 by ABSVALUE:def_2;
now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y))
percases ( y > 0 or y = 0 or y < 0 ) ;
supposeA19: y > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = 1 by ABSVALUE:def_2;
then max ((sgn x),(sgn y)) = 1 by A18, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A19; ::_thesis: verum
end;
supposeA20: y = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = 0 by ABSVALUE:def_2;
then max ((sgn x),(sgn y)) = 0 by A18, XXREAL_0:def_10;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A17, A20; ::_thesis: verum
end;
supposeA21: y < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y))
then sgn y = - 1 by ABSVALUE:def_2;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A9, A17, A18, A21; ::_thesis: verum
end;
end;
end;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum
end;
end;
end;
hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum
end;
hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum
end;
then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22;
hence max ((sgn x),(sgn y)) is_result_of [x,y],M by A1; ::_thesis: verum
end;
registration
let I, O be non empty set ;
cluster non empty calculating_type halting for Moore-SM_Final over I,O;
existence
ex b1 being non empty Moore-SM_Final over I,O st
( b1 is calculating_type & b1 is halting )
proof
set f = the Function of {0,1},O;
take I -TwoStatesMooreSM (0,1, the Function of {0,1},O) ; ::_thesis: ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting )
thus ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting ) ; ::_thesis: verum
end;
end;
registration
let I be non empty set ;
cluster non empty calculating_type halting for SM_Final over I;
existence
ex b1 being non empty SM_Final over I st
( b1 is calculating_type & b1 is halting )
proof
set O = the non empty set ;
set M = the non empty calculating_type halting Moore-SM_Final over I, the non empty set ;
take the non empty calculating_type halting Moore-SM_Final over I, the non empty set ; ::_thesis: ( the non empty calculating_type halting Moore-SM_Final over I, the non empty set is calculating_type & the non empty calculating_type halting Moore-SM_Final over I, the non empty set is halting )
thus ( the non empty calculating_type halting Moore-SM_Final over I, the non empty set is calculating_type & the non empty calculating_type halting Moore-SM_Final over I, the non empty set is halting ) ; ::_thesis: verum
end;
end;
definition
let I, O be non empty set ;
let M be non empty calculating_type halting Moore-SM_Final over I,O;
let s be Element of I;
A1: s leads_to_final_state_of M by Def6;
func Result (s,M) -> Element of O means :Def9: :: FSM_2:def 9
it is_result_of s,M;
uniqueness
for b1, b2 being Element of O st b1 is_result_of s,M & b2 is_result_of s,M holds
b1 = b2 by A1, Th21;
existence
ex b1 being Element of O st b1 is_result_of s,M by A1, Th20;
end;
:: deftheorem Def9 defines Result FSM_2:def_9_:_
for I, O being non empty set
for M being non empty calculating_type halting Moore-SM_Final over I,O
for s being Element of I
for b5 being Element of O holds
( b5 = Result (s,M) iff b5 is_result_of s,M );
theorem :: FSM_2:27
for O, I being non empty set
for s being Element of I
for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
proof
let O, I be non empty set ; ::_thesis: for s being Element of I
for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
let s be Element of I; ::_thesis: for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
let f be Function of {0,1},O; ::_thesis: Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
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 I -TwoStatesMooreSM (0,1,f) by Def6;
A2: the FinalS of (I -TwoStatesMooreSM (0,1,f)) = {1} by Def7;
A3: the OFun of (I -TwoStatesMooreSM (0,1,f)) = f by Def7;
consider m being non empty Element of NAT such that
A4: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) and
A5: for w being FinSequence of I
for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . j in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A1, Th18;
now__::_thesis:_ex_m_being_non_empty_Element_of_NAT_st_
for_w_being_FinSequence_of_I_st_w_._1_=_s_holds_
(_(_m_<=_(len_w)_+_1_implies_(_f_._1_=_the_OFun_of_(I_-TwoStatesMooreSM_(0,1,f))_._((GEN_(w,_the_InitS_of_(I_-TwoStatesMooreSM_(0,1,f))))_._m)_&_(GEN_(w,_the_InitS_of_(I_-TwoStatesMooreSM_(0,1,f))))_._m_in_the_FinalS_of_(I_-TwoStatesMooreSM_(0,1,f))_)_)_&_(_for_n_being_non_empty_Element_of_NAT_st_n_<_m_&_n_<=_(len_w)_+_1_holds_
not_(GEN_(w,_the_InitS_of_(I_-TwoStatesMooreSM_(0,1,f))))_._n_in_the_FinalS_of_(I_-TwoStatesMooreSM_(0,1,f))_)_)
take m = m; ::_thesis: for w being FinSequence of I st w . 1 = s holds
( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) )
let w be FinSequence of I; ::_thesis: ( w . 1 = s implies ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) )
assume A6: w . 1 = s ; ::_thesis: ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) )
hereby ::_thesis: for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f))
assume m <= (len w) + 1 ; ::_thesis: ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) )
then (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A4, A6;
hence ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
thus for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A5, A6; ::_thesis: verum
end;
then f . 01 is_result_of s,I -TwoStatesMooreSM (0,1,f) by Def8;
hence Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 by Def9; ::_thesis: verum
end;
theorem :: FSM_2:28
for M being non empty calculating_type halting 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 being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) holds
for x, y being Element of REAL holds Result ([x,y],M) = max (x,y)
proof
let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds Result ([x,y],M) = max (x,y) )
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 being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x and
A6: for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = max (x,y)
let x, y be Real; ::_thesis: Result ([x,y],M) = max (x,y)
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 Result ([x,y],M) = max (x,y) by A7, Def9; ::_thesis: verum
end;
theorem :: FSM_2:29
for M being non empty calculating_type halting 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 being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) holds
for x, y being Element of REAL holds Result ([x,y],M) = min (x,y)
proof
let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds Result ([x,y],M) = min (x,y) )
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 being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = x and
A6: for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = min (x,y)
let x, y be Real; ::_thesis: Result ([x,y],M) = min (x,y)
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 Result ([x,y],M) = min (x,y) by A7, Def9; ::_thesis: verum
end;
theorem :: FSM_2:30
for M being non empty calculating_type halting 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 being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) holds
for x, y being Element of REAL holds Result ([x,y],M) = x + y
proof
let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) implies for x, y being Element of REAL holds Result ([x,y],M) = x + y )
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 being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = x + y
let x, y be Real; ::_thesis: Result ([x,y],M) = x + y
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 Result ([x,y],M) = x + y by A6, Def9; ::_thesis: verum
end;
theorem :: FSM_2:31
for M being non empty calculating_type halting 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 being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real 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 being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds
for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y))
proof
let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( 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 being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real 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 being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y)) )
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 ; ::_thesis: ( ex x, y being Real st
( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st
( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st
( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y)) )
assume that
A5: for x, y being Real st ( x > 0 or y > 0 ) holds
the Tran of M . [ the InitS of M,[x,y]] = 1 and
A6: for x, y being Real 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 being Real st x < 0 & y < 0 holds
the Tran of M . [ the InitS of M,[x,y]] = - 1 ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y))
let x, y be Real; ::_thesis: Result ([x,y],M) = max ((sgn x),(sgn y))
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 Result ([x,y],M) = max ((sgn x),(sgn y)) by A8, Def9; ::_thesis: verum
end;