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 InitS of (I -TwoStatesMooreSM i,f,o) = i & 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
<= 1 & 1
<= len w )
by NAT_1:13;
then consider WI being
Element of
I,
QI,
QI1 being
State of
(I -TwoStatesMooreSM i,f,o) such that A5:
(
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;
thus
(GEN w,the InitS of (I -TwoStatesMooreSM i,f,o)) . 2
= f
by A2, A3, A5, FUNCOP_1:13;
:: thesis: verum
end;
A6:
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 A7:
k + 1
<= (len w) + 1
;
:: thesis: (GEN w,the InitS of (I -TwoStatesMooreSM i,f,o)) . (k + 1) = f
( 1
<= k &
k <= len w )
by A7, NAT_2:21, XREAL_1:8;
then consider WI being
Element of
I,
QI,
QI1 being
State of
(I -TwoStatesMooreSM i,f,o) such that A8:
(
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 FSM_1:def 2;
thus
(GEN w,the InitS of (I -TwoStatesMooreSM i,f,o)) . (k + 1) = f
by A2, A3, A8, FUNCOP_1:13;
:: thesis: verum
end;
A9:
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, A6);
hence
( not j <= (len w) + 1 or (GEN w,the InitS of (I -TwoStatesMooreSM i,f,o)) . j = f )
by A9; :: thesis: verum