let X be Subset of LTLB_WFF; :: thesis: for f, f2 being FinSequence of LTLB_WFF

for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds

prc0 f2,X,i + n

let f, f2 be FinSequence of LTLB_WFF ; :: thesis: for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds

prc0 f2,X,i + n

let i, n be Nat; :: thesis: ( n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i implies prc0 f2,X,i + n )

assume that

A1: n + (len f) <= len f2 and

A2: for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) and

A3: 1 <= i and

A4: i <= len f ; :: thesis: ( not prc0 f,X,i or prc0 f2,X,i + n )

i + n <= (len f) + n by A4, XREAL_1:6;

then A5: i + n <= len f2 by A1, XXREAL_0:2;

A6: f /. i = f . i by A3, A4, Lm1

.= f2 . (i + n) by A2, A3, A4

.= f2 /. (i + n) by A3, A5, Lm1, NAT_1:12 ;

assume A7: prc0 f,X,i ; :: thesis: prc0 f2,X,i + n

for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds

prc0 f2,X,i + n

let f, f2 be FinSequence of LTLB_WFF ; :: thesis: for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds

prc0 f2,X,i + n

let i, n be Nat; :: thesis: ( n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i implies prc0 f2,X,i + n )

assume that

A1: n + (len f) <= len f2 and

A2: for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) and

A3: 1 <= i and

A4: i <= len f ; :: thesis: ( not prc0 f,X,i or prc0 f2,X,i + n )

i + n <= (len f) + n by A4, XREAL_1:6;

then A5: i + n <= len f2 by A1, XXREAL_0:2;

A6: f /. i = f . i by A3, A4, Lm1

.= f2 . (i + n) by A2, A3, A4

.= f2 /. (i + n) by A3, A5, Lm1, NAT_1:12 ;

assume A7: prc0 f,X,i ; :: thesis: prc0 f2,X,i + n

per cases
( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) by A7;

end;

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) by A7;

suppose
ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) ; :: thesis: prc0 f2,X,i + n

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) ; :: thesis: prc0 f2,X,i + n

then consider j, k being Nat such that

A8: 1 <= j and

A9: j < i and

A10: 1 <= k and

A11: k < i and

A12: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ;

A13: ( 1 <= j + n & j + n < i + n ) by A8, A9, NAT_1:12, XREAL_1:8;

A14: k <= len f by A4, A11, XXREAL_0:2;

then k + n <= (len f) + n by XREAL_1:6;

then A15: k + n <= len f2 by A1, XXREAL_0:2;

A16: j <= len f by A4, A9, XXREAL_0:2;

then j + n <= (len f) + n by XREAL_1:6;

then A17: j + n <= len f2 by A1, XXREAL_0:2;

A18: f /. k = f . k by A10, A14, Lm1

.= f2 . (k + n) by A2, A10, A14

.= f2 /. (k + n) by A10, A15, Lm1, NAT_1:12 ;

A19: ( 1 <= k + n & k + n < i + n ) by A10, A11, NAT_1:12, XREAL_1:8;

f /. j = f . j by A8, A16, Lm1

.= f2 . (j + n) by A2, A8, A16

.= f2 /. (j + n) by A8, A17, Lm1, NAT_1:12 ;

hence prc0 f2,X,i + n by A6, A12, A13, A19, A18; :: thesis: verum

end;A8: 1 <= j and

A9: j < i and

A10: 1 <= k and

A11: k < i and

A12: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ;

A13: ( 1 <= j + n & j + n < i + n ) by A8, A9, NAT_1:12, XREAL_1:8;

A14: k <= len f by A4, A11, XXREAL_0:2;

then k + n <= (len f) + n by XREAL_1:6;

then A15: k + n <= len f2 by A1, XXREAL_0:2;

A16: j <= len f by A4, A9, XXREAL_0:2;

then j + n <= (len f) + n by XREAL_1:6;

then A17: j + n <= len f2 by A1, XXREAL_0:2;

A18: f /. k = f . k by A10, A14, Lm1

.= f2 . (k + n) by A2, A10, A14

.= f2 /. (k + n) by A10, A15, Lm1, NAT_1:12 ;

A19: ( 1 <= k + n & k + n < i + n ) by A10, A11, NAT_1:12, XREAL_1:8;

f /. j = f . j by A8, A16, Lm1

.= f2 . (j + n) by A2, A8, A16

.= f2 /. (j + n) by A8, A17, Lm1, NAT_1:12 ;

hence prc0 f2,X,i + n by A6, A12, A13, A19, A18; :: thesis: verum

suppose
ex j being Nat st

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ; :: thesis: prc0 f2,X,i + n

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ; :: thesis: prc0 f2,X,i + n

then consider j being Nat such that

A20: 1 <= j and

A21: j < i and

A22: ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ;

A23: ( 1 <= j + n & j + n < i + n ) by A20, A21, NAT_1:12, XREAL_1:8;

A24: j <= len f by A4, A21, XXREAL_0:2;

then j + n <= (len f) + n by XREAL_1:6;

then A25: j + n <= len f2 by A1, XXREAL_0:2;

f /. j = f . j by A20, A24, Lm1

.= f2 . (j + n) by A2, A20, A24

.= f2 /. (j + n) by A20, A25, Lm1, NAT_1:12 ;

hence prc0 f2,X,i + n by A6, A22, A23; :: thesis: verum

end;A20: 1 <= j and

A21: j < i and

A22: ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ;

A23: ( 1 <= j + n & j + n < i + n ) by A20, A21, NAT_1:12, XREAL_1:8;

A24: j <= len f by A4, A21, XXREAL_0:2;

then j + n <= (len f) + n by XREAL_1:6;

then A25: j + n <= len f2 by A1, XXREAL_0:2;

f /. j = f . j by A20, A24, Lm1

.= f2 . (j + n) by A2, A20, A24

.= f2 /. (j + n) by A20, A25, Lm1, NAT_1:12 ;

hence prc0 f2,X,i + n by A6, A22, A23; :: thesis: verum