let E be non empty set ; 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); 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; ( 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
; 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; ( 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
; P = Q
per cases
( len P = len Q or len P > len Q or len P < len Q )
by XXREAL_0:1;
suppose A5:
len P > len Q
;
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;
verum end; suppose A9:
len P < len Q
;
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;
verum end;