:: On state machines of calculating type
:: by Hisayoshi Kunimune , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received December 3, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, XBOOLE_0, SUBSET_1, FINSEQ_1, FSM_1, ARYTM_3,
FUNCT_1, XXREAL_0, ORDINAL4, FINSEQ_3, TARSKI, RELAT_1, PARTFUN1, CARD_1,
NAT_1, CARD_5, ZFMISC_1, ARYTM_1, STRUCT_0, GLIB_000, FUNCOP_1, BINOP_1,
ORDINAL1, ABSVALUE, MSUALG_1, FSM_2, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, NAT_1, DOMAIN_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, STRUCT_0,
FSM_1;
constructors REAL_1, SQUARE_1, ABSVALUE, FUNCOP_1, FINSEQ_3, FINSEQ_4,
BORSUK_1, FSM_1, VALUED_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
NAT_1, FINSEQ_1, NAT_2, STRUCT_0, FSM_1, XREAL_0, CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions STRUCT_0, FSM_1, XBOOLE_0;
equalities FSM_1, ORDINAL1;
expansions FSM_1, XBOOLE_0;
theorems NAT_1, NAT_2, FINSEQ_1, PARTFUN1, FINSEQ_2, FINSEQ_3, FSM_1, FUNCT_1,
REWRITE1, WSIERP_1, GRFUNC_1, TREES_1, ZFMISC_1, GRAPH_2, TARSKI,
FUNCOP_1, FUNCT_2, RELAT_1, ABSVALUE, XBOOLE_0, XREAL_1, XXREAL_0,
FINSEQ_4, ORDINAL1, PRE_POLY, XREAL_0, FINSEQ_6;
schemes NAT_1, NAT_2, BINOP_1;
begin :: Calculating type
reserve x,y for Real,
i, j for non zero Element of NAT,
I, O for non empty set,
s,s1,s2,s3 for Element of I,
w, w1, w2 for FinSequence of I,
t for Element of O,
S for non empty FSM over I,
q, q1 for State of S;
notation
let I, S, q, w;
synonym GEN(w,q) for (q,w)-admissible;
end;
registration
let I, S, q, w;
cluster GEN(w, q) -> non empty;
coherence
proof len GEN(w, q) = len w + 1 by FSM_1:def 2;
hence thesis;
end;
end;
theorem Th1:
GEN(<*s*>, q) = <*q, (the Tran of S).[q, s]*>
proof
A1: len <*s*> = 1 by FINSEQ_1:39;
A2: len GEN(<*s*>, q) = len <*s*> + 1 by FSM_1:def 2
.= 2 by A1;
A3: GEN(<*s*>, q).1 = q by FSM_1:def 2;
1 <= len <*s*> by FINSEQ_1:39;
then consider WI 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;
hence thesis by A2,A3,A5,A6,A7,FINSEQ_1:44;
end;
theorem Th2:
GEN(<*s1,s2*>, q) = <*q, (the Tran of S).[q, s1],
(the Tran of S).[(the Tran of S).[q, s1], s2]*>
proof
set w = <*s1,s2*>;
A1: GEN(w,q).1 = q by FSM_1:def 2;
A2: w = <*s1*>^<*s2*> by FINSEQ_1:def 9;
A3: len <*s1*> = 1 by FINSEQ_1:39;
GEN(<*s1*>, q) = <*q, (the Tran of S).[q, s1]*> by Th1;
then GEN(<*s1*>, q).(1+1) = (the Tran of S).[q, s1];
then q, <*s1*>-leads_to ((the Tran of S).[q, s1]) by A3;
then
A4: GEN(w, q).(1+1) = (the Tran of S).[q, s1] by A2,A3,FSM_1:6;
A5: len w = 2 by FINSEQ_1:44;
2 <= len w by FINSEQ_1:44;
then consider WI being Element of I, QI, QI1 being State of S such that
A6: WI = w.2 and
A7: QI = GEN(w, q).2 and
A8: QI1 = GEN(w, q).(2+1) and
A9: WI-succ_of QI = QI1 by FSM_1:def 2;
A10: WI = s2 by A6;
len GEN(w, q) = len w + 1 by FSM_1:def 2
.= 3 by A5;
hence thesis by A1,A4,A7,A8,A9,A10,FINSEQ_1:45;
end;
theorem
GEN(<*s1,s2,s3*>, q) = <*q, (the Tran of S).[q, s1],
(the Tran of S).[(the Tran of S).[q, s1], s2],
(the Tran of S).[(the Tran of S).[(the Tran of S).[q, s1], s2],s3] *>
proof
set w = <*s1,s2,s3*>;
reconsider w1 = <*s1,s2*>, w2 = <*s3*> as FinSequence of I;
set Q = (the Tran of S).[(the Tran of S).[q,s1], s2];
A1: w = w1^w2 by FINSEQ_1:43;
A2: len w1 = 2 by FINSEQ_1:44;
GEN(w1, q) = <*q, (the Tran of S).[q, s1], Q*> by Th2;
then GEN(w1, q).(len w1 + 1) = Q by A2;
then q,w1-leads_to Q;
then
A3: GEN(w, q) = Del(GEN(w1,q),len w1 + 1)^GEN(w2,Q) by A1,FSM_1:8;
Del(GEN(w1,q),len w1 + 1)
= Del(<*q, (the Tran of S).[q,s1], Q*>, 3) by A2,Th2
.= <*q, (the Tran of S).[q,s1]*> by WSIERP_1:19;
then GEN(w, q) = <*q, (the Tran of S).[q,s1]*> ^
<* Q, (the Tran of S).[Q,s3]*> by A3,Th1;
hence thesis by FINSEQ_4:74;
end;
definition
let I, S;
attr S is calculating_type means
for j holds for w1, w2 st w1.1 = w2.1 & j <= len(w1)+1 &
j <= len(w2)+1 holds GEN(w1, the InitS of S).j = GEN(w2, the InitS of S).j;
end;
theorem Th4:
S is calculating_type implies for w1, w2 st w1.1 = w2.1 holds
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable
proof
assume
A1: S is calculating_type;
let w1, w2 such that
A2: w1.1 = w2.1;
set A = Seg(1+len w1) /\ Seg(1+len w2);
1+len w1 <= 1+len w2 or 1+len w2 <= 1+len w1;
then
A3: Seg(1+len w1) c= Seg(1+len w2) & A = Seg(1+len w1) or
Seg(1+len w2) c= Seg(1+len w1) & A = Seg(1+len w2) by FINSEQ_1:5,7;
A4: len GEN(w1, the InitS of S) = 1+len w1 by FSM_1:def 2;
A5: len GEN(w2, the InitS of S) = 1+len w2 by FSM_1:def 2;
A6: dom GEN(w1, the InitS of S) = Seg(1+len w1) by A4,FINSEQ_1:def 3;
A7: dom GEN(w2, the InitS of S) = Seg(1+len w2) by A5,FINSEQ_1:def 3;
now
let x be object;
assume
A8: x in A;
then reconsider i = x as Element of NAT;
A9: i >= 1 by A3,A8,FINSEQ_1:1;
A10: i <= 1+len w1 by A3,A8,FINSEQ_1:1;
i <= 1+len w2 by A3,A8,FINSEQ_1:1;
hence GEN(w1, the InitS of S).x = GEN(w2, the InitS of S).x
by A1,A2,A9,A10;
end;
hence GEN(w1, the InitS of S) c= GEN(w2, the InitS of S) or
GEN(w2, the InitS of S) c= GEN(w1, the InitS of S) by A3,A6,A7,GRFUNC_1:2;
end;
theorem Th5:
(for w1, w2 st w1.1 = w2.1 holds
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable)
implies S is calculating_type
proof
assume
A1: for w1, w2 st w1.1 = w2.1 holds
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable;
let j, w1, w2 such that
A2: w1.1 = w2.1 and
A3: j <= len(w1)+1 and
A4: j <= len(w2)+1;
A5: dom GEN(w1, the InitS of S) =
Seg len(GEN(w1,the InitS of S)) by FINSEQ_1:def 3
.= Seg(len w1 + 1) by FSM_1:def 2;
A6: dom GEN(w2, the InitS of S) =
Seg len(GEN(w2,the InitS of S)) by FINSEQ_1:def 3
.= Seg(len w2 + 1) by FSM_1:def 2;
A7: 1 <= j by NAT_1:14;
then
A8: j in dom GEN(w1, the InitS of S) by A3,A5,FINSEQ_1:1;
j in dom GEN(w2, the InitS of S) by A4,A6,A7,FINSEQ_1:1;
then
A9: j in dom GEN(w1, the InitS of S) /\ dom GEN(w2, the InitS of S)
by A8,XBOOLE_0:def 4;
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable by A1,A2;
then GEN(w1, the InitS of S) c= GEN(w2, the InitS of S) or
GEN(w2, the InitS of S) c= GEN(w1, the InitS of S);
then GEN(w1, the InitS of S) tolerates GEN(w2, the InitS of S)
by PARTFUN1:54;
hence thesis by A9,PARTFUN1:def 4;
end;
theorem
S is calculating_type implies
for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds
GEN(w1, the InitS of S) = GEN(w2, the InitS of S)
proof
assume
A1: S is calculating_type;
let w1,w2;
assume that
A2: w1.1 = w2.1 and
A3: len w1 = len w2;
A4: len GEN(w1, the InitS of S) = 1 + len w1 by FSM_1:def 2;
len GEN(w2, the InitS of S) = 1 + len w2 by FSM_1:def 2;
hence thesis by A1,A2,A3,A4,Th4,TREES_1:4;
end;
Lm1: now
let I, S, w, q;
A1: dom GEN(w, q) = Seg(len GEN(w,q)) by FINSEQ_1:def 3
.= Seg(len w + 1) by FSM_1:def 2;
1 <= len w + 1 by NAT_1:11;
then
A2: 1 in dom GEN(w, q) by A1,FINSEQ_1:1;
GEN(w, q).1 = q by FSM_1:def 2;
then [1,q] in GEN(w, q) by A2,FUNCT_1:def 2;
then {[1,q]} c= GEN(w, q) by ZFMISC_1:31;
then <*q*> c= GEN(w, q) by FINSEQ_1:def 5;
then GEN(<*> I, q) c= GEN(w, q) by FSM_1:1;
hence GEN(<*> I, q), GEN(w, q) are_c=-comparable;
end;
Lm2: now
let p,q be FinSequence such that
A1: p <> {} and
A2: q <> {} and
A3: p.len p = q.1;
consider p1 being FinSequence, x being object such that
A4: p = p1^<*x*> by A1,FINSEQ_1:46;
consider y being object, 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;
end;
theorem Th7:
(for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds
GEN(w1, the InitS of S) = GEN(w2, the InitS of S))
implies S is calculating_type
proof
assume
A1: for w1, w2 st w1.1 = w2.1 & len w1 = len w2 holds
GEN(w1, the InitS of S) = GEN(w2, the InitS of S);
now
let w1, w2;
assume
A2: w1.1 = w2.1;
thus
GEN(w1, the InitS of S), GEN(w2, the InitS of S) are_c=-comparable
proof per cases;
suppose w1 = <*> I or w2 = <*> I;
hence thesis by Lm1;
end;
suppose
A3: w1 <> {} & w2 <> {};
reconsider v1 = w2|Seg len w1, v2 = w1|Seg len w2 as
FinSequence of I by FINSEQ_1:18;
len w1 <= len w2 or len w2 <= len w1;
then
A4: v1 = w2 & len v2 = len w2 & len w1 >= len w2 or
len v1 = len w1 & v2 = w1 & len w1 <= len w2
by FINSEQ_1:17,FINSEQ_2:20;
A5: len w1 >= 0+1 by A3,NAT_1:13;
A6: len w2 >= 0+1 by A3,NAT_1:13;
A7: v1.1 = w2.1 by A4,A5,FINSEQ_6:128;
v2.1 = w1.1 by A4,A6,FINSEQ_6:128;
then
A8: GEN(v1, the InitS of S) = GEN(w1, the InitS of S) or
GEN(v2, the InitS of S) = GEN(w2, the InitS of S) by A1,A2,A4,A7;
consider s1 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, s2 as FinSequence of I by A9,A10,FINSEQ_1:36;
v1 <> {}
proof
assume
A11: v1 = {};
A12: dom v1 = dom w2 /\ Seg len w1 by RELAT_1:61
.= Seg len w2 /\ Seg len w1 by FINSEQ_1:def 3;
len w2 <= len w1 or len w1 <= len w2;
then dom v1 = Seg len w2 or dom v1 = Seg len w1 by A12,FINSEQ_1:7;
then len v1 = len w2 or len v1 = len w1 by FINSEQ_1:def 3;
hence contradiction by A3,A11;
end;
then 1 <= len v1 by NAT_1:14;
then
A13: ex WI being Element of I, 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 = {};
then
A14: len v2 = 0;
A15: dom v2 = dom w1 /\ Seg len w2 by RELAT_1:61
.= Seg len w1 /\ Seg len w2 by FINSEQ_1:def 3;
len w2 <= len w1 or len w1 <= len w2;
then dom v2 = Seg len w2 or dom v2 = Seg len w1 by A15,FINSEQ_1:7;
hence contradiction by A3,A14,FINSEQ_1:def 3;
end;
then 1 <= len v2 by NAT_1:14;
then ex WI2 being Element of I, 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;
then
A20: GEN(w2, the InitS of S)
= Del(GEN(v1, the InitS of S), len v1 + 1)^GEN(s1, q1) by A9,FSM_1:8
.= GEN(v1, the InitS of S)^Del(GEN(s1, q1),1) by A16,A18,Lm2;
the InitS of S, v2-leads_to q2;
then GEN(w1, the InitS of S)
= Del(GEN(v2, the InitS of S), len v2 + 1)^GEN(s2, q2) by A10,FSM_1:8
.= GEN(v2, the InitS of S)^Del(GEN(s2, q2),1) by A17,A19,Lm2;
then GEN(w1, the InitS of S) c= GEN(w2, the InitS of S) or
GEN(w2, the InitS of S) c= GEN(w1, the InitS of S)
by A8,A20,TREES_1:1;
hence thesis;
end;
end;
end;
hence thesis by Th5;
end;
definition
let I, S, q, s;
pred q is_accessible_via s means
ex w be FinSequence of I st the InitS of S,<*s*>^w-leads_to q;
end;
definition
let I, S, q;
attr q is accessible means
ex w be FinSequence of I st the InitS of S,w-leads_to q;
end;
theorem
q is_accessible_via s implies q is accessible;
theorem
q is accessible & q <> the InitS of S implies ex s st q is_accessible_via s
proof
assume that
A1: q is accessible and
A2: q <> the InitS of S;
consider W be FinSequence of I such that
A3: the InitS of S,W-leads_to q by A1;
W <> {}
by FSM_1:def 2,A2,A3;
then consider S 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;
thus thesis by A3,A4;
end;
theorem
the InitS of S is accessible
proof
set w = <*>I;
GEN(w, the InitS of S).(len w+1) = the InitS of S by FSM_1:def 2;
then the InitS of S,w-leads_to the InitS of S;
hence thesis;
end;
theorem
S is calculating_type & q is_accessible_via s implies
ex m being non zero Element of NAT st
for w st len w+1 >= m & w.1 = s holds q = GEN(w, the InitS of S).m &
for i st i < m holds GEN(w, the InitS of S).i <> q
proof
assume
A1: S is calculating_type;
given w being FinSequence of I such that
A2: the InitS of S, <*s*>^w-leads_to q;
defpred P[Nat] means
q = GEN(<*s*>^w, the InitS of S).$1 & $1 >= 1 & $1 <= len(<*s*>^w)+1;
A3: len(<*s*>^w)+1 >= 1 by NAT_1:11;
q = GEN(<*s*>^w, the InitS of S).(len(<*s*>^w)+1 ) by A2;
then
A4: ex m being Nat st P[m] by A3;
consider m being Nat such that
A5: P[m] and
A6: for k being Nat st P[k] holds m <= k from NAT_1:sch 5(A4);
reconsider m as non zero Element of NAT by A5,ORDINAL1:def 12;
take m;
let w1 such that
A7: len w1+1 >= m and
A8: w1.1 = s;
(<*s*>^w).1 = s by FINSEQ_1:41;
then GEN(w1, the InitS of S), GEN(<*s*>^w, the InitS of S) are_c=-comparable
by A1,A8,Th4;
then
A9: GEN(w1, the InitS of S) c= GEN(<*s*>^w, the InitS of S) or
GEN(<*s*>^w, the InitS of S) c= GEN(w1, the InitS of S);
A10: dom(GEN(<*s*>^w, the InitS of S))
= Seg(len GEN(<*s*>^w, the InitS of S)) by FINSEQ_1:def 3
.= Seg(len(<*s*>^w)+1) by FSM_1:def 2;
A11: dom(GEN(w1, the InitS of S))
= Seg(len GEN(w1, the InitS of S)) by FINSEQ_1:def 3
.= Seg(len w1 + 1) by FSM_1:def 2;
A12: m in dom GEN(<*s*>^w, the InitS of S) by A5,A10,FINSEQ_1:1;
m in dom GEN(w1, the InitS of S) by A5,A7,A11,FINSEQ_1:1;
hence q = GEN(w1, the InitS of S).m by A5,A9,A12,GRFUNC_1:2;
let i;
assume
A13: i < m;
A14: 1 <= i by NAT_1:14;
A15: i <= len(<*s*>^w)+1 by A5,A13,XXREAL_0:2;
A16: i <= len w1 + 1 by A7,A13,XXREAL_0:2;
A17: dom GEN(w1, the InitS of S)
= Seg(len GEN(w1, the InitS of S)) by FINSEQ_1:def 3
.= Seg(len w1 + 1) by FSM_1:def 2;
dom GEN(<*s*>^w, the InitS of S)
= Seg(len GEN(<*s*>^w, the InitS of S)) by FINSEQ_1:def 3
.= Seg(len(<*s*>^w)+1) by FSM_1:def 2;
then
A18: i in dom GEN(<*s*>^w, the InitS of S) by A14,A15,FINSEQ_1:1;
A19: i in dom GEN(w1, the InitS of S) by A14,A16,A17,FINSEQ_1:1;
assume GEN(w1, the InitS of S).i = q;
then q = GEN(<*s*>^w, the InitS of S).i by A9,A18,A19,GRFUNC_1:2;
hence thesis by A6,A13,A14,A15;
end;
definition
let I, S;
attr S is regular means
for q being State of S holds q is accessible;
end;
theorem
(for s1,s2,q holds (the Tran of S).[q,s1] = (the Tran of S).[ q,s2]) implies
S is calculating_type
proof
assume
A1: for s1,s2,q holds (the Tran of S).[q,s1] = (the Tran of S).[q,s2];
for j holds for w1,w2 st w1.1 = w2.1 & j <= len(w1)+1 & j <= len(w2)+1 holds
GEN(w1, the InitS of S).j = GEN(w2, the InitS of S).j
proof
let j;
let w1,w2;
assume that
A2: w1.1 = w2.1 and
A3: j <= len(w1)+1 and
A4: j <= len(w2)+1;
defpred P[Nat] means for w1,w2 st w1.1 = w2.1 &
$1 <= len(w1) + 1 & $1 <= len(w2) + 1
holds GEN(w1, the InitS of S).$1 = GEN(w2, the InitS of S).$1;
A5: P[1]
proof
let w1,w2;
GEN(w1, the InitS of S).1 = the InitS of S by FSM_1:def 2;
hence thesis by FSM_1:def 2;
end;
A6: for h being non zero Nat st P[h] holds P[h+1]
proof
let h be non zero Nat;
assume
A7: for w1,w2 st w1.1 = w2.1 & h <= len(w1)+1 & h <= len(w2)+1 holds
GEN(w1, the InitS of S).h = GEN(w2, the InitS of S).h;
let w1,w2;
assume that
A8: w1.1 = w2.1 and
A9: h+1 <= len(w1)+1 and
A10: h+1 <= len(w2)+1;
A11: h <= len(w1) by A9,XREAL_1:6;
A12: h <= len(w1)+1 by A9,NAT_1:13;
1 <= h by NAT_1:14;
then consider WI 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 thesis by A1,A14,A15,A19,A20;
end;
for j being non zero Nat holds P[j] from NAT_1:sch 10(A5,A6);
hence thesis by A2,A3,A4;
end;
hence thesis;
end;
theorem
for S st (for s1,s2,q st q<>the InitS of S holds
(the Tran of S).[q,s1] = (the Tran of S).[q,s2]) & for s,q1 holds
(the Tran of S).[q1,s] <> the InitS of S holds S is calculating_type
proof
let S;
assume that
A1: for s1,s2,q st q<>the InitS of S holds (the Tran of S).[q,s1] = (the
Tran of S).[q,s2] and
A2: for s,q1 holds (the Tran of S).[q1,s] <> the InitS of S;
A3: for j st j >= 2 holds for w1 st j <= len(w1)+1 holds
GEN(w1, the InitS of S).j <> the InitS of S
proof
let j;
assume j >= 2;
then j <> 1;
then
A4: j is non trivial by NAT_2:def 1;
defpred P[Nat] means for w1 st $1 <= len w1 + 1 holds
GEN(w1, the InitS of S).$1 <> the InitS of S;
A5: P[2]
proof
let w1;
assume 2 <= len(w1) + 1;
then 1 + 1 <= len(w1) + 1;
then 1 <= len(w1) by XREAL_1:6;
then ex WI being Element of I, 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 thesis by A2;
end;
A6: for h being non trivial Nat st P[h] holds P[h+1]
proof
let h be non trivial Nat;
assume for w1 st h <= len(w1)+1 holds
GEN(w1, the InitS of S).h <> the InitS of S;
let w1;
assume
A7: h+1 <= len(w1)+1;
A8: 1 <= h by NAT_1:14;
h <= len(w1) by A7,XREAL_1:6;
then ex WI being Element of I, 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 thesis by A2;
end;
for h being non trivial Nat holds P[h] from NAT_2:sch 2(A5,A6);
hence thesis by A4;
end;
for j holds for w1,w2 st w1.1 = w2.1 & j <= len(w1)+1 & j <= len(w2)+1 holds
GEN(w1, the InitS of S).j = GEN(w2, the InitS of S).j
proof
let j;
let w1,w2;
assume that
A9: w1.1 = w2.1 and
A10: j <= len(w1)+1 and
A11: j <= len(w2)+1;
defpred P[Nat] means for w1,w2 st w1.1 = w2.1 &
$1 <= len(w1) + 1 & $1 <= len(w2) + 1
holds GEN(w1, the InitS of S).$1 = GEN(w2, the InitS of S).$1;
A12: P[1]
proof
let w1,w2;
GEN(w1, the InitS of S).1 = the InitS of S by FSM_1:def 2;
hence thesis by FSM_1:def 2;
end;
A13: for h being non zero Nat st P[h] holds P[h+1]
proof
let h be non zero Nat;
assume
A14: for w1,w2 st w1.1 = w2.1 & h <= len(w1)+1 & h <= len(w2)+1 holds
GEN(w1, the InitS of S).h = GEN(w2, the InitS of S).h;
let w1,w2;
assume that
A15: w1.1 = w2.1 and
A16: h+1 <= len(w1)+1 and
A17: h+1 <= len(w2)+1;
A18: h <= len(w1) by A16,XREAL_1:6;
A19: h <= len(w1)+1 by A16,NAT_1:13;
A20: 1 <= h by NAT_1:14;
then consider WI 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 thesis by A1,A3,A15,A19,A21,A22,A23,A24,A27,A29,A30,A31,A32;
end;
for j being non zero Nat holds P[j] from NAT_1:sch 10(A12,A13);
hence thesis by A9,A10,A11;
end;
hence thesis;
end;
theorem Th14:
S is regular & S is calculating_type implies
for s1, s2, q st q<>the InitS of S holds GEN(<*s1*>,q).2 = GEN(<*s2*>,q).2
proof
assume that
A1: S is regular and
A2: S is calculating_type;
let s1, s2, q;
assume
A3: q<>the InitS of S;
q is accessible by A1;
then consider w such that
A4: the InitS of S,w-leads_to q;
w <> {}
by FSM_1:def 2,A3,A4;
then consider x 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*>, w2 = w^<*s2*>;
len <*x*> = 1 by FINSEQ_1:39;
then len <*x*> + len w9 >= 1 by NAT_1:11;
then len w >= 1 by A5,FINSEQ_1:22;
then
A6: 1 in dom w by FINSEQ_3:25;
then w.1 = w1.1 by FINSEQ_1:def 7;
then
A7: w1.1 = w2.1 by A6,FINSEQ_1:def 7;
A8: len <*s1*> = 1 by FINSEQ_1:39;
then
A9: len w1 = len w + 1 by FINSEQ_1:22;
A10: len <*s2*> = 1 by FINSEQ_1:39;
then
A11: len w2 = len w + 1 by FINSEQ_1:22;
A12: len w1 = len w2 by A9,A10,FINSEQ_1:22;
set p = Del(GEN(w, the InitS of S), len w + 1);
set p1 = GEN(<*s1*>, q);
A13: GEN(w1, the InitS of S) = p^p1 by A4,FSM_1:8;
A14: len(GEN(w, the InitS of S)) = len w + 1 by FSM_1:def 2;
then
A15: len p = len w by PRE_POLY:12;
A16: len p1 = len(<*s1*>) + 1 by FSM_1:def 2
.= 1 + 1 by FINSEQ_1:39;
A17: len(GEN(w1, the InitS of S)) = len(p^p1) by A4,FSM_1:8
.= len p + len p1 by FINSEQ_1:22
.= len w + (1 + 1) by A14,A16,PRE_POLY:12
.= (len w + 1) + 1
.= len w1 + 1 by A8,FINSEQ_1:22;
A18: len p + 1 <= len w1 + 1 by A9,A15,NAT_1:11;
len(p^p1) = len w1 + 1 by A4,A17,FSM_1:8;
then len p + len p1 = len w1 + 1 by FINSEQ_1:22;
then
A19: GEN(w1,the InitS of S).(len w1 + 1)=p1.((len w1 + 1) - len p)
by A13,A18,FINSEQ_1:23
.= p1.((len w1 + 1) - len w) by A14,PRE_POLY:12
.= p1.((len w + 1 + 1) - len w) by A8,FINSEQ_1:22
.= p1.2;
set p2 = GEN(<*s2*>, q);
A20: GEN(w2, the InitS of S) = p^p2 by A4,FSM_1:8;
A21: len p2 = len(<*s2*>) + 1 by FSM_1:def 2
.= 1 + 1 by FINSEQ_1:39;
A22: len(GEN(w2, the InitS of S)) = len(p^p2) by A4,FSM_1:8
.= len p + len p2 by FINSEQ_1:22
.= len w + (1 + 1) by A14,A21,PRE_POLY:12
.= (len w + 1) + 1
.= len w2 + 1 by A10,FINSEQ_1:22;
len w + 1 <= len w2 + 1 by A11,NAT_1:11;
then
A23: len p + 1 <= len w2 + 1 by A14,PRE_POLY:12;
len(p^p2) = len w2 + 1 by A4,A22,FSM_1:8;
then len w2 + 1 <= len p + len p2 by FINSEQ_1:22;
then GEN(w2,the InitS of S).(len w2 + 1)=p2.((len w2 + 1) - len p)
by A20,A23,FINSEQ_1:23
.= p2.((len w2 + 1) - len w) by A14,PRE_POLY:12
.= p2.((len w + 1 + 1) - len w) by A10,FINSEQ_1:22
.= p2.2;
hence thesis by A2,A7,A12,A19;
end;
theorem
S is regular & S is calculating_type implies
for s1, s2, q st q<>the InitS of S holds
(the Tran of S).[q,s1] = (the Tran of S).[q,s2]
proof
assume that
A1: S is regular and
A2: S is calculating_type;
let s1, s2, q;
assume
A3: q<>the InitS of S;
set w1=<*s1*>;
set w2=<*s2*>;
A4: len w1 = 0+1 by FINSEQ_1:39;
reconsider j = len w1 as non zero Element of NAT;
consider WI being Element of I, QI, QI1 being State of S such that
A5: WI = w1.j and
A6: QI = GEN(w1, q).j and
A7: QI1 = GEN(w1, q).(j+1) and
A8: WI-succ_of QI = QI1 by A4,FSM_1:def 2;
WI = s1 by A4,A5;
then
A9: QI1 = s1-succ_of q by A4,A6,A8,FSM_1:def 2;
A10: len w2 = 0+1 by FINSEQ_1:39;
reconsider h = len w2 as non zero Element of NAT;
consider WI2 being Element of I, QI2, QI12 being State of S such that
A11: WI2 = w2.h and
A12: QI2 = GEN(w2, q).h and
A13: QI12 = GEN(w2, q).(h+1) and
A14: WI2-succ_of QI2 = QI12 by A10,FSM_1:def 2;
A15: QI2 = q by A10,A12,FSM_1:def 2;
WI2 = s2 by A10,A11;
hence thesis by A1,A2,A3,A4,A7,A9,A10,A13,A14,A15,Th14;
end;
theorem
S is regular & S is calculating_type implies for s, s1, s2, q st
(the Tran of S).[the InitS of S,s1] <>
(the Tran of S).[the InitS of S,s2] holds
(the Tran of S).[q,s] <> the InitS of S
proof
assume that
A1: S is regular and
A2: S is calculating_type;
let s, s1, s2, q;
assume
A3: (the Tran of S).[the InitS of S,s1] <> (the Tran of S).[the InitS of S,s2];
q is accessible by A1;
then consider w such that
A4: the InitS of S, w-leads_to q;
A5: GEN(w, the InitS of S).(len w + 1) = q by A4;
assume
A6: (the Tran of S).[q,s]=the InitS of S;
reconsider w1 = <*s,s1*>, w2 = <*s,s2*> as FinSequence of I;
A7: GEN(w1,q) = <* q, the InitS of S,
(the Tran of S).[the InitS of S,s1] *> by A6,Th2;
A8: GEN(w2,q) = <* q, the InitS of S,
(the Tran of S).[the InitS of S,s2] *> by A6,Th2;
A9: GEN(w1, q).3 = (the Tran of S).[the InitS of S,s1] by A7;
A10: GEN(w2, q).3 = (the Tran of S).[the InitS of S,s2] by A8;
A11: len w1 = 2 by FINSEQ_1:44;
A12: len w2 = 2 by FINSEQ_1:44;
A13: 3 <= len w1 +1 by A11;
A14: 3 <= len w2+1 by A12;
A15: GEN(w^w1, the InitS of S).(len w+3) = (the Tran of S).[the InitS of S,
s1] by A4,A9,A13,FSM_1:7;
A16: GEN(w^w2, the InitS of S).(len w+3) = (the Tran of S).[the InitS of S,
s2] by A4,A10,A14,FSM_1:7;
per cases;
suppose w = {};
then
A17: len w = 0;
A18: GEN(w1, the InitS of S) = <* the InitS of S, (the Tran of S).[the InitS
of S,s], (the Tran of S).[(the Tran of S).[the InitS of S,s], s1]*> by Th2;
A19: GEN(w2, the InitS of S) = <* the InitS of S, (the Tran of S).[the InitS
of S,s], (the Tran of S).[(the Tran of S).[the InitS of S,s], s2]*> by Th2;
A20: w1.1 = s;
A21: w2.1 = s;
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
.= (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
.= (the Tran of S).[the InitS of S, s2]
by A5,A6,A17,FSM_1:def 2;
hence contradiction by A2,A3,A20,A21,A22,A23,A24;
end;
suppose w <> {};
then consider s9 being object, 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;
A28: dom <*s9*> c= dom w by A25,FINSEQ_1:26;
then
A29: (w^w1).1 = s9 by A26,A27,FINSEQ_1:def 7;
A30: (w^w2).1 = s9 by A26,A27,A28,FINSEQ_1:def 7;
A31: len(w^w1)+1 = (len w+2)+1 by A11,FINSEQ_1:22;
len(w^w2)+1 = (len w+2)+1 by A12,FINSEQ_1:22;
hence contradiction by A2,A3,A15,A16,A29,A30,A31;
end;
end;
begin :: Machines with final states
definition
let I be set;
struct (FSM over I) SM_Final over I (# carrier -> set,
Tran -> Function of [: the carrier, I :], the carrier,
InitS -> Element of the carrier, FinalS -> Subset of the carrier #);
end;
registration
let I be set;
cluster non empty for SM_Final over I;
existence
proof
set A = the non empty set,T = the Function of [: A, I :], A,I = the Element of
A,F = the Subset of A;
take S = SM_Final (# A, T, I, F#);
thus the carrier of S is non empty;
end;
end;
definition
let I, s;
let S be non empty SM_Final over I;
pred s leads_to_final_state_of S means
ex q being State of S st q is_accessible_via s & q in the FinalS of S;
end;
definition
let I;
let S be non empty SM_Final over I;
attr S is halting means
:Def6:
s leads_to_final_state_of S;
end;
definition
let I be set, O be non empty set;
struct (SM_Final over I, Moore-FSM over I, O) Moore-SM_Final over I,O (#
carrier -> set, Tran -> Function of [: the carrier, I :], the carrier,
OFun -> Function of the carrier, O, InitS -> Element of the carrier,
FinalS -> Subset of the carrier #);
end;
registration
let I be set, O be non empty set;
cluster non empty strict for Moore-SM_Final over I, O;
existence
proof
set A = the non empty set,T = the Function of [: A, I :], A,o = the Function of
A, O,I = the Element of A,F = the Subset of A;
take S = Moore-SM_Final (# A, T, o, I, F #);
thus the carrier of S is non empty;
thus thesis;
end;
end;
definition
let I, O;
let i,f be set;
let o be Function of {i,f}, O;
func I-TwoStatesMooreSM(i,f,o) -> non empty strict Moore-SM_Final over I, O
means
:Def7:
the carrier of it = {i,f} &
the Tran of it = [:{i,f}, I :] --> f & the OFun of it = o &
the InitS of it = i & the FinalS of it = {f};
uniqueness;
existence
proof
set X = {i,f};
reconsider ii = i, ff = f as Element of X by TARSKI:def 2;
reconsider oo = o as Function of X, O;
Moore-SM_Final(# X, [:X, I:] --> ff, oo, ii, {ff} #) is non empty;
hence thesis;
end;
end;
theorem Th17:
for i,f being set, o being Function of {i,f}, O
for j st 1 < j & j <= len w+1 holds
GEN(w, the InitS of I-TwoStatesMooreSM(i,f,o)).j = f
proof
let i,f being set, o being Function of {i,f},O;
let j;
assume
A1: 1 < j;
set M = I-TwoStatesMooreSM(i,f,o);
A2: the carrier of M = {i, f} by Def7;
A3: the Tran of M = [:{i, f}, I:] --> f by Def7;
defpred P[Nat] means $1 <= len w + 1 implies
GEN(w, the InitS of I-TwoStatesMooreSM(i,f,o)).$1 = f;
A4: P[2]
proof
assume 2 <= len w + 1;
then 1+1 <= len w+1;
then 1 < len w+1 by NAT_1:13;
then 1 <= len w by NAT_1:13;
then ex WI being Element of I, 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;
hence thesis by A2,A3,FUNCOP_1:7;
end;
A5: for k be non trivial Nat st P[k] holds P[k+1]
proof
let k be non trivial Nat;
assume that k <= len w + 1 implies GEN(w, the InitS of M).k = f and
A6: k+1 <= len w + 1;
A7: 1 <= k by NAT_2:19;
k <= len w by A6,XREAL_1:6;
then ex WI being Element of I, QI, QI1 being State of M st ( WI
= w.k)&( QI = GEN(w, the InitS of M).k)&( QI1 = GEN(w, the InitS of M).(k+1))&(
WI-succ_of QI = QI1) by A7,FSM_1:def 2;
hence thesis by A2,A3,FUNCOP_1:7;
end;
A8: j is non trivial Nat by A1,NAT_2:def 1;
for k be non trivial Nat holds P[k] from NAT_2:sch 2(A4,A5);
hence thesis by A8;
end;
registration
let I, O;
let i,f be set;
let o be Function of {i,f}, O;
cluster I-TwoStatesMooreSM(i,f,o) -> calculating_type;
coherence
proof
set M = I-TwoStatesMooreSM(i,f,o);
for w1,w2 st w1.1 = w2.1 & len w1 = len w2 holds
GEN(w1, the InitS of M) = GEN(w2, the InitS of M)
proof
let w1,w2;
assume that
w1.1 = w2.1 and
A1: len w1 = len w2;
reconsider p = GEN(w1, the InitS of M),
q = GEN(w2, the InitS of M) as FinSequence;
A2: p.1 = the InitS of M by FSM_1:def 2
.= q.1 by FSM_1:def 2;
A3: len p = len w1 + 1 by FSM_1:def 2;
A4: len q = len w1 + 1 by A1,FSM_1:def 2;
now
let j be Nat;
assume
A5: 1 <= j;
A6: j in NAT by ORDINAL1:def 12;
j = 1 or j > 1 by A5,XXREAL_0:1;
then p.j = q.j or (j <= len p implies p.j = f & q.j = f)
by A1,A2,A3,A6,Th17;
hence j <= len p implies p.j = q.j;
end;
hence thesis by A3,A4,FINSEQ_1:14;
end;
hence thesis by Th7;
end;
end;
registration
let I, O;
let i,f be set;
let o be Function of {i,f}, O;
cluster I-TwoStatesMooreSM(i,f,o) -> halting;
coherence
proof
let s;
{i,f} = the carrier of I-TwoStatesMooreSM(i,f,o) by Def7;
then reconsider q = f as State of I-TwoStatesMooreSM(i,f,o) by TARSKI:def 2;
take q;
thus q is_accessible_via s
proof
take w = <*> I;
<*s*>^w = <*s*> by FINSEQ_1:34;
then len (<*s*>^w) = 1 by FINSEQ_1:39;
hence GEN(<*s*>^w,
the InitS of I-TwoStatesMooreSM(i,f,o)).(len (<*s*>^w)+1) = q by Th17;
end;
the FinalS of I-TwoStatesMooreSM(i,f,o) = {f} by Def7;
hence thesis by TARSKI:def 1;
end;
end;
reserve n, m, o, p for non zero Element of NAT,
M for non empty Moore-SM_Final over I, O,
q for State of M;
theorem Th18:
M is calculating_type & s leads_to_final_state_of M implies
ex m being non zero Element of NAT st
(for w st len w+1 >= m & w.1 = s holds
GEN(w, the InitS of M).m in the FinalS of M) &
for w,j st j <= len w +1 & w.1 = s & j < m holds
not GEN(w, the InitS of M).j in the FinalS of M
proof
assume
A1: M is calculating_type;
given q such that
A2: q is_accessible_via s and
A3: q in the FinalS of M;
consider w such that
A4: the InitS of M,<*s*>^w-leads_to q by A2;
defpred P[Nat] means GEN(<*s*>^w, the InitS of M).$1 in the FinalS of M &
$1 >= 1 & $1 <= len(<*s*>^w)+1;
A5: len(<*s*>^w)+1 >= 1 by NAT_1:11;
q = GEN(<*s*>^w, the InitS of M).(len(<*s*>^w)+1 ) by A4;
then
A6: ex m being Nat st P[m] by A3,A5;
consider m being Nat such that
A7: P[m] and
A8: for k being Nat st P[k] holds m <= k from NAT_1:sch 5(A6);
reconsider m as non zero Element of NAT by A7,ORDINAL1:def 12;
take m;
hereby
let w1 such that
A9: len w1+1 >= m and
A10: w1.1 = s;
(<*s*>^w).1 = s by FINSEQ_1:41;
then GEN(w1, the InitS of M), GEN(<*s*>^w, the InitS of M)
are_c=-comparable by A1,A10,Th4;
then
A11: GEN(w1, the InitS of M) c= GEN(<*s*>^w, the InitS of M) or
GEN(<*s*>^w, the InitS of M) c= GEN(w1, the InitS of M);
A12: dom(GEN(<*s*>^w, the InitS of M))
= Seg(len GEN(<*s*>^w, the InitS of M)) by FINSEQ_1:def 3
.= Seg(len(<*s*>^w)+1) by FSM_1:def 2;
A13: dom(GEN(w1, the InitS of M))
= Seg(len GEN(w1, the InitS of M)) by FINSEQ_1:def 3
.= Seg(len w1 + 1) by FSM_1:def 2;
A14: m in dom GEN(<*s*>^w, the InitS of M) by A7,A12,FINSEQ_1:1;
m in dom GEN(w1, the InitS of M) by A7,A9,A13,FINSEQ_1:1;
hence GEN(w1, the InitS of M).m in the FinalS of M by A7,A11,A14,GRFUNC_1:2
;
end;
let w1;
let i;
assume that
A15: i <= len w1 + 1 and
A16: w1.1 = s and
A17: i < m;
(<*s*>^w).1 = s by FINSEQ_1:41;
then GEN(w1, the InitS of M), GEN(<*s*>^w, the InitS of M) are_c=-comparable
by A1,A16,Th4;
then
A18: GEN(w1, the InitS of M) c= GEN(<*s*>^w, the InitS of M) or
GEN(<*s*>^w, the InitS of M) c= GEN(w1, the InitS of M);
A19: 1 <= i by NAT_1:14;
A20: i <= len(<*s*>^w)+1 by A7,A17,XXREAL_0:2;
A21: dom GEN(w1, the InitS of M)
= Seg(len GEN(w1, the InitS of M)) by FINSEQ_1:def 3
.= Seg(len w1 + 1) by FSM_1:def 2;
dom GEN(<*s*>^w, the InitS of M)
= Seg(len GEN(<*s*>^w, the InitS of M)) by FINSEQ_1:def 3
.= Seg(len(<*s*>^w)+1) by FSM_1:def 2;
then
A22: i in dom GEN(<*s*>^w, the InitS of M) by A19,A20,FINSEQ_1:1;
A23: i in dom GEN(w1, the InitS of M) by A15,A19,A21,FINSEQ_1:1;
assume GEN(w1, the InitS of M).i in the FinalS of M;
then GEN(<*s*>^w, the InitS of M).i in the FinalS of M
by A18,A22,A23,GRFUNC_1:2;
hence thesis by A8,A17,A19,A20;
end;
begin :: Correctness of a result of state machine
definition
let I, O, M, s;
let t be object;
pred t is_result_of s,M means
ex m st for w st w.1=s holds
(m <= len w+1 implies t = (the OFun of M).(GEN(w, the InitS of M).m) &
GEN(w, the InitS of M).m in the FinalS of M) &
for n st n < m & n <= len w+1 holds
not GEN(w, the InitS of M).n in the FinalS of M;
end;
theorem
the InitS of M in the FinalS of M implies
(the OFun of M).the InitS of M is_result_of s, M
proof
assume
A1: the InitS of M in the FinalS of M;
take 1;
let w;
assume w.1 = s;
thus thesis by A1,FSM_1:def 2,NAT_1:14;
end;
theorem Th20:
M is calculating_type & s leads_to_final_state_of M
implies ex t st t is_result_of s, M
proof
assume that
A1: M is calculating_type and
A2: s leads_to_final_state_of M;
consider q such that
A3: q is_accessible_via s and
A4: q in the FinalS of M by A2;
consider w such that
A5: the InitS of M,<*s*>^w-leads_to q by A3;
A6: GEN(<*s*>^w, the InitS of M).(len(<*s*>^w)+1) = q by A5;
consider m being non zero Element of NAT such that
A7: for w st len w+1 >= m & w.1 = s holds GEN(w, the InitS of M).m in the
FinalS of M and
A8: for w,j st j <= len w +1 & w.1 = s & j < m holds not GEN(w, the
InitS of M).j in the FinalS of M
by A1,A2,Th18;
A9: (<*s*>^w).1 = s by FINSEQ_1:41;
then
A10: len(<*s*>^w)+1 >= m by A4,A6,A8;
then GEN(<*s*>^w, the InitS of M).m in the FinalS of M by A7,A9;
then reconsider t = (the OFun of M).(GEN(<*s*>^w, the InitS of M).m)
as Element of O by FUNCT_2:5;
take t, m;
let w1 such that
A11: w1.1=s;
(<*s*>^w).1 = s by FINSEQ_1:41;
hence m <= len w1+1 implies t = (the OFun of M).(GEN(w1, the InitS of M).m) &
GEN(w1, the InitS of M).m in the FinalS of M by A1,A7,A10,A11;
thus thesis by A8,A11;
end;
theorem Th21:
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
proof
assume that
A1: s leads_to_final_state_of M;
let t1, t2 being Element of O;
given m such that
A2: for w1 st w1.1=s holds (m <= len w1+1 implies
t1 = (the OFun of M).(GEN(w1, the InitS of M).m) &
GEN(w1, the InitS of M).m in the FinalS of M) &
for n st n < m & n <= len w1+1 holds
not GEN(w1, the InitS of M).n in the FinalS of M;
given o such that
A3: for w2 st w2.1=s holds (o <= len w2+1 implies
t2 = (the OFun of M).(GEN(w2, the InitS of M).o) &
GEN(w2, the InitS of M).o in the FinalS of M) &
for p st p < o & p <= len w2+1 holds
not GEN(w2, the InitS of M).p in the FinalS of M;
consider q being State of M such that
A4: q is_accessible_via s and
A5: q in the FinalS of M by A1;
consider w being FinSequence of I such that
A6: the InitS of M,<*s*>^w-leads_to q by A4;
set w1 = <*s*>^w;
A7: GEN(w1, the InitS of M).(len w1+1) = q by A6;
A8: (<*s*>^w).1 = s by FINSEQ_1:41;
then
A9: len(<*s*>^w)+1 >= m by A2,A5,A7;
A10: o <= len w1+1 by A3,A5,A7,A8;
A11: o < m or o = m or o > m by XXREAL_0:1;
A12: w1.1 = s by FINSEQ_1:41;
then
A13: t1 = (the OFun of M).(GEN(w1, the InitS of M).m) by A2,A9;
A14: GEN(w1, the InitS of M).m in the FinalS of M by A2,A9,A12;
GEN(w1, the InitS of M).o in the FinalS of M by A3,A10,A12;
hence thesis by A2,A3,A9,A10,A11,A12,A13,A14;
end;
theorem Th22:
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, f be BinOp of X;
let M be non empty Moore-SM_Final over [:X, X:], succ X;
assume that
A1: M is calculating_type and
A2: the carrier of M = succ X and
A3: the FinalS of M = X and
A4: the InitS of M = X and
A5: the OFun of M = id the carrier of M and
A6: for x,y being Element of X holds (the Tran of M).[the InitS of M, [x
,y]] = f.(x,y);
A7: not the InitS of M in the FinalS of M by A3,A4;
thus
A8: now
let s be Element of [:X,X:];
consider x,y being object such that
A9: x in X and
A10: y in X and
A11: s = [x,y] by ZFMISC_1:def 2;
reconsider x,y as Element of X by A9,A10;
thus s leads_to_final_state_of M
proof
reconsider q = f.(x,y) as State of M by A2,XBOOLE_0:def 3;
take q;
thus q is_accessible_via s
proof
take w = <*> [:X, X:];
reconsider W = <*s*>^w as FinSequence of [:X, X:];
A12: W = <*[x,y]*> by A11,FINSEQ_1:34;
then len W = 1 by FINSEQ_1:39;
then
A13: ex WI being Element of [:X, X:], 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 thesis;
end;
thus thesis by A3;
end;
end;
let x,y be Element of X;
consider m being non zero 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:], i being non zero Element of NAT
st i <= len w + 1 & w.1 = [x,y] & i < m holds
not GEN(w, the InitS of M).i in the FinalS of M by A1,A8,Th18;
take m;
set s = [x,y], t = f.(x,y);
let w being FinSequence of [:X, X:] such that
A16: w.1 = s;
hereby
assume
A17: m <= len w + 1;
GEN(w, the InitS of M).1 = X by A4,FSM_1:def 2;
then
A18: m <> 1 by A4,A7,A14,A16,A17;
m >= 1 by NAT_1:14;
then m > 1 by A18,XXREAL_0:1;
then
A19: m >= 1+1 by NAT_1:13;
then
A20: 1 + 1 <= len w + 1 by A17,XXREAL_0:2;
then 1 <= len w by XREAL_1:6;
then ex WI being Element of [:X, X:], 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 t = (the OFun of M).(GEN(w, the InitS of M).m)
by A2,A3,A5,A15,A16,A20,A21,A22,FUNCT_1:18;
thus GEN(w, the InitS of M).m in the FinalS of M by A14,A16,A17;
end;
thus thesis by A15,A16;
end;
theorem Th23:
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 st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds max(x,y) is_result_of [x,y], M
proof
deffunc F(Real,Real) = In(max($1,$2),REAL);
consider f being BinOp of REAL such that
A1: for x,y being Element of REAL holds f.(x,y) = F(x,y)
from BINOP_1:sch 4;
A2: for x,y being Element of REAL holds f.(x,y) = max(x,y)
proof let x,y be Element of REAL;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
let M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A3: M is calculating_type and
A4: the carrier of M = succ REAL and
A5: the FinalS of M = REAL and
A6: the InitS of M = REAL and
A7: the OFun of M = id the carrier of M;
assume that
A8: for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x and
A9: for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y;
let x,y be Element of REAL;
reconsider x,y as Element of REAL;
now
let x,y be Element of REAL;
A10: x >= y implies (the Tran of M).[the InitS of M, [x,y]] = x by A8;
x < y implies (the Tran of M).[the InitS of M, [x,y]] = y by A9;
then (the Tran of M).[the InitS of M, [x,y]] = max(x,y) by A10,
XXREAL_0:def 10;
hence (the Tran of M).[the InitS of M, [x,y]] = f.(x,y) by A2;
end;
then f.(x,y) is_result_of [x,y], M by A3,A4,A5,A6,A7,Th22;
hence thesis by A2;
end;
theorem Th24:
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 st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds min(x,y) is_result_of [x,y], M
proof
deffunc F(Real, Real) = In(min($1,$2),REAL);
consider f being BinOp of REAL such that
A1: for x,y being Element of REAL holds f.(x,y) = F(x,y)
from BINOP_1:sch 4;
A2: for x,y being Element of REAL holds f.(x,y) = min(x,y)
proof let x,y be Element of REAL;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
let M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A3: M is calculating_type and
A4: the carrier of M = succ REAL and
A5: the FinalS of M = REAL and
A6: the InitS of M = REAL and
A7: the OFun of M = id the carrier of M;
assume that
A8: for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x and
A9: for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y;
let x,y be Element of REAL;
now
let x,y be Element of REAL;
A10: x < y implies (the Tran of M).[the InitS of M, [x,y]] = x by A8;
x >= y implies (the Tran of M).[the InitS of M, [x,y]] = y by A9;
then (the Tran of M).[the InitS of M, [x,y]] = min(x,y) by A10,
XXREAL_0:def 9;
hence (the Tran of M).[the InitS of M, [x,y]] = f.(x,y) by A2;
end;
then f.(x,y) is_result_of [x,y], M by A3,A4,A5,A6,A7,Th22;
hence thesis by A2;
end;
theorem Th25:
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 holds (the Tran of M).[the InitS of M, [x,y]] = x+y)
for x,y being Element of REAL holds x+y is_result_of [x,y], M
proof
deffunc F(Real,Real) = In($1+$2,REAL);
consider f being BinOp of REAL such that
A1: for x,y being Element of REAL holds f.(x,y) = F(x,y)
from BINOP_1:sch 4;
A2: for x,y being Element of REAL holds f.(x,y) = x+y
proof let x,y be Element of REAL;
reconsider x,y as Real;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
let M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A3: M is calculating_type and
A4: the carrier of M = succ REAL and
A5: the FinalS of M = REAL and
A6: the InitS of M = REAL and
A7: the OFun of M = id the carrier of M;
assume
A8: for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x + y;
let x,y be Element of REAL;
now
let x,y be Element of REAL;
(the Tran of M).[the InitS of M, [x,y]] = x+y by A8;
hence (the Tran of M).[the InitS of M, [x,y]] = f.(x,y) by A2;
end;
then f.(x,y) is_result_of [x,y], M by A3,A4,A5,A6,A7,Th22;
hence thesis by A2;
end;
theorem Th26:
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 st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1) &
(for x,y st (x=0 or y=0) & x <= 0 & y <=0
holds (the Tran of M).[the InitS of M, [x,y]] = 0) &
(for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1)
for x,y being Element of REAL holds max(sgn x,sgn y) is_result_of [x,y], M
proof
deffunc F(Real,Real) = In(max(sgn $1,sgn $2),REAL);
consider f being BinOp of REAL such that
A1: for x,y being Element of REAL holds f.(x,y) = F(x,y)
from BINOP_1:sch 4;
A2: for x,y being Element of REAL holds f.(x,y) = max(sgn x,sgn y)
proof let x,y be Element of REAL;
reconsider x,y as Real;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
let M being non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A3: M is calculating_type and
A4: the carrier of M = succ REAL and
A5: the FinalS of M = REAL and
A6: the InitS of M = REAL and
A7: the OFun of M = id the carrier of M;
assume that
A8: for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1 and
A9: for x,y st (x=0 or y=0) & x <= 0 & y <=0 holds (the Tran of M).[the
InitS of M, [x,y]] = 0 and
A10: for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1;
let x,y be Element of REAL;
now
let x,y be Element of REAL;
(the Tran of M).[the InitS of M, [x,y]] = F(x,y)
proof
now per cases;
suppose
A11: x > 0;
then
A12: sgn x = 1 by ABSVALUE:def 2;
now per cases;
suppose y > 0;
then sgn y = 1 by ABSVALUE:def 2;
hence thesis by A8,A11,A12;
end;
suppose y = 0;
then sgn y = 0 by ABSVALUE:def 2;
then max(sgn x, sgn y) = 1 by A12,XXREAL_0:def 10;
hence thesis by A8,A11;
end;
suppose y < 0;
then sgn y = -1 by ABSVALUE:def 2;
then max(sgn x, sgn y) = 1 by A12,XXREAL_0:def 10;
hence thesis by A8,A11;
end;
end;
hence thesis;
end;
suppose
A13: x = 0;
then
A14: sgn x = 0 by ABSVALUE:def 2;
now per cases;
suppose
A15: y > 0;
then sgn y = 1 by ABSVALUE:def 2;
then max(sgn x, sgn y) = 1 by A14,XXREAL_0:def 10;
hence thesis by A8,A15;
end;
suppose
A16: y = 0;
then sgn y = 0 by ABSVALUE:def 2;
hence thesis by A9,A13,A16;
end;
suppose
A17: y < 0;
then sgn y = -1 by ABSVALUE:def 2;
then max(sgn x, sgn y) = 0 by A14,XXREAL_0:def 10;
hence thesis by A9,A13,A17;
end;
end;
hence thesis;
end;
suppose
A18: x < 0;
then
A19: sgn x = -1 by ABSVALUE:def 2;
now per cases;
suppose
A20: y > 0;
then sgn y = 1 by ABSVALUE:def 2;
then max(sgn x, sgn y) = 1 by A19,XXREAL_0:def 10;
hence thesis by A8,A20;
end;
suppose
A21: y = 0;
then sgn y = 0 by ABSVALUE:def 2;
then max(sgn x, sgn y) = 0 by A19,XXREAL_0:def 10;
hence thesis by A9,A18,A21;
end;
suppose
A22: y < 0;
then sgn y = -1 by ABSVALUE:def 2;
hence thesis by A10,A18,A19,A22;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence (the Tran of M).[the InitS of M, [x,y]] = f.(x,y) by A2;
end;
then f.(x,y) is_result_of [x,y], M by A3,A4,A5,A6,A7,Th22;
hence thesis by A2;
end;
registration
let I, O;
cluster calculating_type halting for non empty Moore-SM_Final over I, O;
existence
proof set f = the Function of {0, 1}, O;
take I-TwoStatesMooreSM(0,1,f);
thus thesis;
end;
end;
registration
let I;
cluster calculating_type halting for non empty SM_Final over I;
existence
proof set O = the non empty set;
set M = the calculating_type halting non empty Moore-SM_Final over I, O;
take M;
thus thesis;
end;
end;
definition
let I, O;
let M be calculating_type halting non empty Moore-SM_Final over I, O;
let s;
A1: s leads_to_final_state_of M by Def6;
func Result(s, M) -> Element of O means
:Def9:
it is_result_of s, M;
uniqueness by A1,Th21;
existence by A1,Th20;
end;
theorem
for f being Function of {0, 1}, O holds
Result(s, I-TwoStatesMooreSM(0,1,f)) = f.1
proof
let f being Function of {0, 1}, O;
set M = I-TwoStatesMooreSM(0,1,f);
reconsider 01 = 1 as Element of {0, 1} by TARSKI:def 2;
A1: s leads_to_final_state_of M by Def6;
A2: the FinalS of M = {1} by Def7;
A3: the OFun of M = f by Def7;
consider m being non zero Element of NAT such that
A4: for w st len w+1 >= m & w.1 = s holds
GEN(w, the InitS of M).m in the FinalS of M and
A5: for w,j st j <= len w +1 & w.1 = s & j < m holds
not GEN(w, the InitS of M).j in the FinalS of M by A1,Th18;
now
take m;
let w;
assume
A6: w.1 = s;
hereby
assume m <= len w + 1;
then GEN(w, the InitS of M).m in the FinalS of M by A4,A6;
hence f.1 = (the OFun of M).(GEN(w, the InitS of M).m) &
GEN(w, the InitS of M).m in the FinalS of M by A2,A3,TARSKI:def 1;
end;
thus for n st n < m & n <= len w + 1 holds
not GEN(w, the InitS of M).n in the FinalS of M by A5,A6;
end;
then f.01 is_result_of s,M;
hence thesis by Def9;
end;
theorem
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds Result([x,y], M) = max(x,y)
proof
let M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A1: the carrier of M = succ REAL and
A2: the FinalS of M = REAL and
A3: the InitS of M = REAL and
A4: the OFun of M = id the carrier of M and
A5: for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = x and
A6: for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = y;
let x,y be Element of REAL;
max(x,y) in REAL by XREAL_0:def 1;
then
A7: max(x,y) in succ REAL by XBOOLE_0:def 3;
max(x,y) is_result_of [x,y], M by A1,A2,A3,A4,A5,A6,Th23;
hence thesis by A7,Def9;
end;
theorem
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x) &
(for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y)
for x,y being Element of REAL holds Result([x,y], M) = min(x,y)
proof
let M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A1: the carrier of M = succ REAL and
A2: the FinalS of M = REAL and
A3: the InitS of M = REAL and
A4: the OFun of M = id the carrier of M and
A5: for x,y st x < y holds (the Tran of M).[the InitS of M, [x,y]] = x and
A6: for x,y st x >= y holds (the Tran of M).[the InitS of M, [x,y]] = y;
let x,y be Element of REAL;
min(x,y) in REAL by XREAL_0:def 1;
then
A7: min(x,y) in succ REAL by XBOOLE_0:def 3;
min(x,y) is_result_of [x,y], M by A1,A2,A3,A4,A5,A6,Th24;
hence thesis by A7,Def9;
end;
theorem
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x+y)
for x,y being Element of REAL holds Result([x,y], M) = x+y
proof
let M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A1: the carrier of M = succ REAL and
A2: the FinalS of M = REAL and
A3: the InitS of M = REAL and
A4: the OFun of M = id the carrier of M and
A5: for x,y holds (the Tran of M).[the InitS of M, [x,y]] = x+y;
let x,y be Element of REAL;
A6: x+y in succ REAL by XBOOLE_0:def 3;
x+y is_result_of [x,y], M by A1,A2,A3,A4,A5,Th25;
hence thesis by A6,Def9;
end;
theorem
for M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL
st the carrier of M = succ REAL & the FinalS of M = REAL &
the InitS of M = REAL & the OFun of M = id the carrier of M &
(for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1) &
(for x,y st (x=0 or y=0) & x <= 0 & y <=0
holds (the Tran of M).[the InitS of M, [x,y]] = 0) &
(for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1)
for x,y being Element of REAL holds Result([x,y], M) = max(sgn x, sgn y)
proof
let M being calculating_type halting
non empty Moore-SM_Final over [:REAL, REAL:], succ REAL;
assume that
A1: the carrier of M = succ REAL and
A2: the FinalS of M = REAL and
A3: the InitS of M = REAL and
A4: the OFun of M = id the carrier of M;
assume that
A5: for x,y st x>0 or y>0 holds (the Tran of M).[the InitS of M, [x,y]] = 1 and
A6: for x,y st (x=0 or y=0) & x <= 0 & y <=0 holds (the Tran of M).[the
InitS of M, [x,y]] = 0 and
A7: for x,y st x<0 & y<0 holds (the Tran of M).[the InitS of M, [x,y]] = -1;
let x,y be Element of REAL;
max(sgn x, sgn y) in REAL by XREAL_0:def 1;
then
A8: max(sgn x, sgn y) in succ REAL by XBOOLE_0:def 3;
max(sgn x, sgn y) is_result_of [x,y], M by A1,A2,A3,A4,A5,A6,A7,Th26;
hence thesis by A8,Def9;
end;