let w be Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]; ( ex p being State of s ex y being Symbol of s st
( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) & ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] implies ( w = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff w = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) ) )
thus
( ex p being State of s ex y being Symbol of s st
( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) & ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] implies ( w = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff w = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) ) )
verumproof
given p being
State of
s,
y being
Symbol of
s such that A1:
x = [[p, the InitS of t],y]
and A2:
p <> the
AcceptS of
s
;
( for q being State of t
for y being Symbol of t holds not x = [[ the AcceptS of s,q],y] or ( w = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff w = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) ) )
given q being
State of
t,
z being
Symbol of
t such that A3:
x = [[ the AcceptS of s,q],z]
;
( w = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff w = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) )
[p, the InitS of t] = [ the AcceptS of s,q]
by A1, A3, XTUPLE_0:1;
hence
(
w = FirstTuringTran (
s,
t,
( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff
w = SecondTuringTran (
s,
t,
( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) )
by A2, XTUPLE_0:1;
verum
end;