let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
let TS be non empty transition-system over F; :: thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q )
assume A1: TS is deterministic ; :: thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
then A2: not <%> E in rng (dom the Tran of TS) ;
let P, Q be RedSequence of ==>.-relation TS; :: thesis: ( P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 implies P = Q )
assume that
A3: P . 1 = Q . 1 and
A4: (P . (len P)) `2 = (Q . (len Q)) `2 ; :: thesis: P = Q

per cases ( len P = len Q or len P > len Q or len P < len Q ) by XXREAL_0:1;

suppose len P = len Q ; :: thesis: P = Q

hence P = Q by A1, A3, Th68; :: thesis: verum

end;

suppose A5: len P > len Q ; :: thesis: P = Q

len P >= 0 + 1 by NAT_1:13;
then A6: len P in dom P by FINSEQ_3:25;
set k = len Q;
A7: len Q >= 0 + 1 by NAT_1:13;
then A8: len Q in dom P by A5, FINSEQ_3:25;
len Q in dom Q by A7, FINSEQ_3:25;
then (P . (len Q)) `2 = (P . (len P)) `2 by A1, A3, A4, A8, Th67;
hence P = Q by A2, A5, A8, A6, Th66; :: thesis: verum

end;

suppose A9: len P < len Q ; :: thesis: P = Q

len Q >= 0 + 1 by NAT_1:13;
then A10: len Q in dom Q by FINSEQ_3:25;
set k = len P;
A11: len P >= 0 + 1 by NAT_1:13;
then A12: len P in dom Q by A9, FINSEQ_3:25;
len P in dom P by A11, FINSEQ_3:25;
then (Q . (len P)) `2 = (Q . (len Q)) `2 by A1, A3, A4, A12, Th67;
hence P = Q by A2, A9, A12, A10, Th66; :: thesis: verum

end;

end;