let E be non empty set ; for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
let F be Subset of (E ^omega); for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
let TS be non empty transition-system over F; ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1 )
assume A1:
not <%> E in rng (dom the Tran of TS)
; for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
let P be RedSequence of ==>.-relation TS; ( (P . 1) `2 = (P . (len P)) `2 implies len P = 1 )
assume A2:
(P . 1) `2 = (P . (len P)) `2
; len P = 1
per cases
( len P <= 1 or len P > 1 )
;
suppose A4:
len P > 1
;
len P = 1then reconsider p1 =
(len P) - 1 as
Nat by NAT_1:21;
A5:
p1 + 1
= len P
;
then A6:
p1 <= len P
by NAT_1:13;
1
+ 1
<= len P
by A4, NAT_1:13;
then A7:
1
+ 1
in dom P
by FINSEQ_3:25;
0 + 1
<= p1 + 1
by XREAL_1:6;
then A8:
p1 + 1
in dom P
by FINSEQ_3:25;
1
<= p1
by A4, A5, NAT_1:13;
then
p1 in dom P
by A6, FINSEQ_3:25;
then consider s2 being
Element of
TS,
v2 being
Element of
E ^omega ,
t2 being
Element of
TS,
w2 being
Element of
E ^omega such that
P . p1 = [s2,v2]
and A9:
P . (p1 + 1) = [t2,w2]
by A8, Th47;
1
in dom P
by A4, FINSEQ_3:25;
then consider s1 being
Element of
TS,
v1 being
Element of
E ^omega ,
t1 being
Element of
TS,
w1 being
Element of
E ^omega such that A10:
P . 1
= [s1,v1]
and
P . (1 + 1) = [t1,w1]
by A7, Th47;
(P . (len P)) `2 = w2
by A9;
then
v1 = w2
by A2, A10;
hence
len P = 1
by A1, A10, A9, Th60;
verum end;