let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( InputVertices S2 c= InputVertices S1 & S = S1 +* S2 implies for A1 being non-empty Circuit of non-empty
for A2 being non-empty Circuit of non-empty
for A being non-empty Circuit of non-empty st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of
for s1 being State of
for s2 being State of st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s1) +* (Following s2) )
assume InputVertices S2 c= InputVertices S1 ; :: thesis: ( not S = S1 +* S2 or for A1 being non-empty Circuit of non-empty
for A2 being non-empty Circuit of non-empty
for A being non-empty Circuit of non-empty st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of
for s1 being State of
for s2 being State of st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s1) +* (Following s2) )
then InnerVertices S1 misses InputVertices S2 by XBOOLE_1:63, XBOOLE_1:79;
hence ( not S = S1 +* S2 or for A1 being non-empty Circuit of non-empty
for A2 being non-empty Circuit of non-empty
for A being non-empty Circuit of non-empty st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of
for s1 being State of
for s2 being State of st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 holds
Following s = (Following s1) +* (Following s2) ) by Th39; :: thesis: verum