let IAlph, OAlph be non empty set ; :: thesis: for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent holds
tfsm1,tfsm3 -are_equivalent
let tfsm1, tfsm2, tfsm3 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: ( tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent implies tfsm1,tfsm3 -are_equivalent )
assume that
A1: tfsm1,tfsm2 -are_equivalent and
A2: tfsm2,tfsm3 -are_equivalent ; :: thesis: tfsm1,tfsm3 -are_equivalent
let w1 be FinSequence of IAlph; :: according to FSM_1:def 9 :: thesis: ( the InitS of tfsm1,w1) -response = ( the InitS of tfsm3,w1) -response
set IS3 = the InitS of tfsm3;
set IS1 = the InitS of tfsm1;
set IS2 = the InitS of tfsm2;
thus ( the InitS of tfsm1,w1) -response = ( the InitS of tfsm2,w1) -response by A1, Def9
.= ( the InitS of tfsm3,w1) -response by A2, Def9 ; :: thesis: verum