let I, O 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 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: 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 S_{1}[ Nat] means ( $1 <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . $1 = f );

A4: S_{1}[2]
_{1}[k] holds

S_{1}[k + 1]

for k being non trivial Nat holds S_{1}[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

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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: 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 S

A4: S

proof

A5:
for k being non trivial Nat st S
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;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

S

proof

A8:
j is non trivial Nat
by A1, NAT_2:def 1;
let k be non trivial Nat; :: thesis: ( S_{1}[k] implies S_{1}[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;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

for k being non trivial Nat holds S

hence ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f ) by A8; :: thesis: verum