set M = I -TwoStatesMooreSM (i,f,o);
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o)))
proof
let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) )
assume that
w1 . 1 = w2 . 1 and
A1: len w1 = len w2 ; :: thesis: GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o)))
reconsider p = GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))), q = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) as FinSequence ;
A2: p . 1 = the InitS of (I -TwoStatesMooreSM (i,f,o)) 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 :: thesis: for j being Nat st 1 <= j & j <= len p holds
p . j = q . j
let j be Nat; :: thesis: ( 1 <= j & j <= len p implies p . j = q . j )
assume A5: 1 <= j ; :: thesis: ( j <= len p implies p . j = q . j )
A6: j in NAT by ORDINAL1:def 12;
( j = 1 or j > 1 ) by A5, XXREAL_0:1;
then not ( not p . j = q . j & j <= len p & not ( p . j = f & q . j = f ) ) by A1, A2, A3, A6, Th17;
hence ( j <= len p implies p . j = q . j ) ; :: thesis: verum
end;
hence GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) by A3, A4, FINSEQ_1:14; :: thesis: verum
end;
hence I -TwoStatesMooreSM (i,f,o) is calculating_type by Th7; :: thesis: verum