let y be object ; for E being non empty set
for w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let E be non empty set ; for w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let w be Element of E ^omega ; for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let F be Subset of (E ^omega); for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let TS be non empty transition-system over F; for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let P be RedSequence of ==>.-relation TS; ( P . (len P) = [y,w] implies for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w )
assume
P . (len P) = [y,w]
; for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
then A1: (P . (len P)) `2 =
{} ^ w
.=
(<%> E) ^ w
;
defpred S1[ Nat] means ( (len P) - $1 in dom P implies ex u being Element of E ^omega st (P . ((len P) - $1)) `2 = u ^ w );
A2:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A3:
S1[
k]
;
S1[k + 1]now ( (len P) - (k + 1) in dom P implies ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w )set len2 =
(len P) - k;
set len1 =
(len P) - (k + 1);
A4:
((len P) - (k + 1)) + 1
= (len P) - k
;
assume A5:
(len P) - (k + 1) in dom P
;
ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ wthus
ex
u being
Element of
E ^omega st
(P . ((len P) - (k + 1))) `2 = u ^ w
verumproof
per cases
( (len P) - k in dom P or not (len P) - k in dom P )
;
suppose A6:
(len P) - k in dom P
;
ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ wthen consider u1 being
Element of
E ^omega such that A7:
(P . ((len P) - k)) `2 = u1 ^ w
by A3;
A8:
[(P . ((len P) - (k + 1))),(P . ((len P) - k))] in ==>.-relation TS
by A5, A4, A6, REWRITE1:def 2;
then consider x being
Element of
TS,
v1 being
Element of
E ^omega ,
y being
Element of
TS,
v2 being
Element of
E ^omega such that A9:
P . ((len P) - (k + 1)) = [x,v1]
and A10:
P . ((len P) - k) = [y,v2]
by Th31;
x,
v1 ==>. y,
v2,
TS
by A8, A9, A10, Def4;
then consider u2 being
Element of
E ^omega such that
x,
u2 -->. y,
TS
and A11:
v1 = u2 ^ v2
;
take
u2 ^ u1
;
(P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w(P . ((len P) - (k + 1))) `2 =
u2 ^ v2
by A9, A11
.=
u2 ^ (u1 ^ w)
by A7, A10
.=
(u2 ^ u1) ^ w
by AFINSQ_1:27
;
hence
(P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w
;
verum end;
end; end; hence
S1[
k + 1]
;
verum end;
A12:
S1[ 0 ]
by A1;
A13:
for k being Nat holds S1[k]
from NAT_1:sch 2(A12, A2);