let I, O 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 zero 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 zero 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;

hence Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 by Def9; :: thesis: verum

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 zero 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 zero 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 zero 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 zero 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)) ) )

then
f . 01 is_result_of s,I -TwoStatesMooreSM (0,1,f)
;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 zero 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 zero 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 zero 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 zero 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)) ) )

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;( ( 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 zero 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 zero 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 zero 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 zero 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))

thus
for n being non zero 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;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

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

hence Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 by Def9; :: thesis: verum