consider fs1 being object such that

A1: fs1 in R1 by XBOOLE_0:def 1;

consider fs2 being object such that

A2: fs2 in R2 by XBOOLE_0:def 1;

reconsider fs1 = fs1, fs2 = fs2 as firing-sequence of N by A1, A2;

reconsider C = fs1 ^ fs2 as firing-sequence of N ;

A3: C = fs1 \/ ((len fs1) Shift fs2) by VALUED_1:49;

A4: fs1 misses (len fs1) Shift fs2 by VALUED_1:50;

A5: fs1 = Seq fs1 by FINSEQ_3:116;

Seq ((len fs1) Shift fs2) in R2 by A2, VALUED_1:46;

then C in R1 concur R2 by A1, A3, A4, A5;

hence not R1 concur R2 is empty ; :: thesis: verum

A1: fs1 in R1 by XBOOLE_0:def 1;

consider fs2 being object such that

A2: fs2 in R2 by XBOOLE_0:def 1;

reconsider fs1 = fs1, fs2 = fs2 as firing-sequence of N by A1, A2;

reconsider C = fs1 ^ fs2 as firing-sequence of N ;

A3: C = fs1 \/ ((len fs1) Shift fs2) by VALUED_1:49;

A4: fs1 misses (len fs1) Shift fs2 by VALUED_1:50;

A5: fs1 = Seq fs1 by FINSEQ_3:116;

Seq ((len fs1) Shift fs2) in R2 by A2, VALUED_1:46;

then C in R1 concur R2 by A1, A3, A4, A5;

hence not R1 concur R2 is empty ; :: thesis: verum