let A be RelStr ; :: thesis: for s being FinSequence of A holds

( s is ascending iff Rev s is descending )

let s be FinSequence of A; :: thesis: ( s is ascending iff Rev s is descending )

( s is ascending iff Rev s is descending )

let s be FinSequence of A; :: thesis: ( s is ascending iff Rev s is descending )

hereby :: thesis: ( Rev s is descending implies s is ascending )

assume A9:
Rev s is descending
; :: thesis: s is ascending assume A1:
s is ascending
; :: thesis: Rev s is descending

end;now :: thesis: for n, m being Nat st n in dom (Rev s) & m in dom (Rev s) & n < m holds

(Rev s) /. m <~ (Rev s) /. n

hence
Rev s is descending
; :: thesis: verum(Rev s) /. m <~ (Rev s) /. n

let n, m be Nat; :: thesis: ( 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 ; :: thesis: (Rev s) /. m <~ (Rev s) /. n

set 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; :: thesis: verum

end;assume that

A2: ( n in dom (Rev s) & m in dom (Rev s) ) and

A3: n < m ; :: thesis: (Rev s) /. m <~ (Rev s) /. n

set 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; :: thesis: verum

now :: thesis: for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. n <~ s /. m

hence
s is ascending
; :: thesis: verums /. n <~ s /. m

let n, m be Nat; :: thesis: ( 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 ; :: thesis: s /. n <~ s /. m

set 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; :: thesis: verum

end;assume that

A10: ( n in dom s & m in dom s ) and

A11: n < m ; :: thesis: s /. n <~ s /. m

set 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; :: thesis: verum