let A be RelStr ; for s being FinSequence of A holds
( s is ascending iff Rev s is descending )
let s be FinSequence of A; ( s is ascending iff Rev s is descending )
hereby ( Rev s is descending implies s is ascending )
assume A1:
s is
ascending
;
Rev s is descending now for n, m being Nat st n in dom (Rev s) & m in dom (Rev s) & n < m holds
(Rev s) /. m <~ (Rev s) /. nlet n,
m be
Nat;
( n in dom (Rev s) & m in dom (Rev s) & n < m implies (Rev s) /. m <~ (Rev s) /. n )assume that A2:
(
n in dom (Rev s) &
m in dom (Rev s) )
and A3:
n < m
;
(Rev s) /. m <~ (Rev s) /. nset l =
len s;
A4:
(
n in dom s &
m in dom s )
by A2, FINSEQ_5:57;
then A5:
(
n in Seg (len s) &
m in Seg (len s) )
by FINSEQ_1:def 3;
then
(
n <= len s &
m <= len s )
by FINSEQ_1:1;
then reconsider a =
((len s) - n) + 1,
b =
((len s) - m) + 1 as
Nat by FINSEQ_5:1;
(
a in Seg (len s) &
b in Seg (len s) )
by A5, FINSEQ_5:2;
then A6:
(
a in dom s &
b in dom s )
by FINSEQ_1:def 3;
A7:
s /. b =
s . b
by A6, PARTFUN1:def 6
.=
(Rev s) . m
by A4, FINSEQ_5:58
.=
(Rev s) /. m
by A2, PARTFUN1:def 6
;
A8:
s /. a =
s . a
by A6, PARTFUN1:def 6
.=
(Rev s) . n
by A4, FINSEQ_5:58
.=
(Rev s) /. n
by A2, PARTFUN1:def 6
;
(
a = ((len s) + 1) - n &
b = ((len s) + 1) - m )
;
then
b < a
by A3, XREAL_1:15;
then
s /. b <~ s /. a
by A1, A6;
hence
(Rev s) /. m <~ (Rev s) /. n
by A7, A8;
verum end; hence
Rev s is
descending
;
verum
end;
assume A9:
Rev s is descending
; s is ascending
now for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <~ s /. mlet n,
m be
Nat;
( n in dom s & m in dom s & n < m implies s /. n <~ s /. m )assume that A10:
(
n in dom s &
m in dom s )
and A11:
n < m
;
s /. n <~ s /. mset l =
len (Rev s);
(
n in dom (Rev s) &
m in dom (Rev s) )
by A10, FINSEQ_5:57;
then A12:
(
n in Seg (len (Rev s)) &
m in Seg (len (Rev s)) )
by FINSEQ_1:def 3;
then
(
n <= len (Rev s) &
m <= len (Rev s) )
by FINSEQ_1:1;
then reconsider a =
((len (Rev s)) - n) + 1,
b =
((len (Rev s)) - m) + 1 as
Nat by FINSEQ_5:1;
A13:
dom s = dom (Rev s)
by FINSEQ_5:57;
(
a in Seg (len (Rev s)) &
b in Seg (len (Rev s)) )
by A12, FINSEQ_5:2;
then A14:
(
a in dom s &
b in dom s )
by A13, FINSEQ_1:def 3;
A15:
s /. n =
(Rev (Rev s)) . n
by A10, PARTFUN1:def 6
.=
(Rev s) . a
by A13, A10, FINSEQ_5:58
.=
(Rev s) /. a
by A14, A13, PARTFUN1:def 6
;
A16:
s /. m =
(Rev (Rev s)) . m
by A10, PARTFUN1:def 6
.=
(Rev s) . b
by A13, A10, FINSEQ_5:58
.=
(Rev s) /. b
by A14, A13, PARTFUN1:def 6
;
(
a = ((len (Rev s)) + 1) - n &
b = ((len (Rev s)) + 1) - m )
;
then
b < a
by A11, XREAL_1:15;
hence
s /. n <~ s /. m
by A15, A16, A9, A13, A14;
verum end;
hence
s is ascending
; verum