let I, O be 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 zero 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; for i, f being set
for o being Function of {i,f},O
for j being non zero 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 ; for o being Function of {i,f},O
for j being non zero 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; for j being non zero 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 zero Element of NAT ; ( 1 < j & j <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f )
assume A1:
1 < j
; ( 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
;
(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;
verum
end;
A5:
for k being non trivial Nat st S1[k] holds
S1[k + 1]
proof
let k be non
trivial Nat;
( 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
;
(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;
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; verum