let X be Subset of LTLB_WFF; :: thesis: for f, f1, f2 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,X,i ) holds

for i being Nat st 1 <= i & i <= len f2 holds

prc f2,X,i

let f, f1, f2 be FinSequence of LTLB_WFF ; :: thesis: ( f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,X,i ) implies for i being Nat st 1 <= i & i <= len f2 holds

prc f2,X,i )

assume that

A1: f2 = f ^ f1 and

1 <= len f and

1 <= len f1 and

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

prc f,X,i and

A3: for i being Nat st 1 <= i & i <= len f1 holds

prc f1,X,i ; :: thesis: for i being Nat st 1 <= i & i <= len f2 holds

prc f2,X,i

A4: len f2 = (len f) + (len f1) by A1, FINSEQ_1:22;

A5: for k being Nat st 1 <= k & k <= len f1 holds

f1 . k = f2 . (k + (len f)) by A1, FINSEQ_1:65;

let i be Nat; :: thesis: ( 1 <= i & i <= len f2 implies prc f2,X,i )

assume that

A6: 1 <= i and

A7: i <= len f2 ; :: thesis: prc f2,X,i

prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,X,i ) holds

for i being Nat st 1 <= i & i <= len f2 holds

prc f2,X,i

let f, f1, f2 be FinSequence of LTLB_WFF ; :: thesis: ( f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,X,i ) implies for i being Nat st 1 <= i & i <= len f2 holds

prc f2,X,i )

assume that

A1: f2 = f ^ f1 and

1 <= len f and

1 <= len f1 and

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

prc f,X,i and

A3: for i being Nat st 1 <= i & i <= len f1 holds

prc f1,X,i ; :: thesis: for i being Nat st 1 <= i & i <= len f2 holds

prc f2,X,i

A4: len f2 = (len f) + (len f1) by A1, FINSEQ_1:22;

A5: for k being Nat st 1 <= k & k <= len f1 holds

f1 . k = f2 . (k + (len f)) by A1, FINSEQ_1:65;

let i be Nat; :: thesis: ( 1 <= i & i <= len f2 implies prc f2,X,i )

assume that

A6: 1 <= i and

A7: i <= len f2 ; :: thesis: prc f2,X,i

per cases
( i <= len f or (len f) + 1 <= i )
by NAT_1:13;

end;

suppose A8:
i <= len f
; :: thesis: prc f2,X,i

then A9: f /. i =
f . i
by A6, Lm1

.= f2 . i by A1, A6, A8, FINSEQ_1:64

.= f2 /. i by A6, A7, Lm1 ;

end;.= f2 . i by A1, A6, A8, FINSEQ_1:64

.= f2 /. i by A6, A7, Lm1 ;

per cases
( f . i in LTL_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 IND_rule f /. i ) ) or ex j being Nat st

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A2, A6, A8, Def29;

end;

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

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A2, A6, A8, Def29;

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 IND_rule f /. i ) ) ; :: thesis: prc f2,X,i

( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; :: thesis: prc f2,X,i

then consider j, k being Nat such that

A10: 1 <= j and

A11: j < i and

A12: 1 <= k and

A13: k < i and

A14: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;

A15: k <= len f by A8, A13, XXREAL_0:2;

then A16: k <= len f2 by A4, NAT_1:12;

A17: f /. k = f . k by A12, A15, Lm1

.= f2 . k by A1, A12, A15, FINSEQ_1:64

.= f2 /. k by A12, A16, Lm1 ;

A18: j <= len f by A8, A11, XXREAL_0:2;

then A19: j <= len f2 by A4, NAT_1:12;

f /. j = f . j by A10, A18, Lm1

.= f2 . j by A1, A10, A18, FINSEQ_1:64

.= f2 /. j by A10, A19, Lm1 ;

hence prc f2,X,i by A9, A10, A11, A12, A13, A14, A17; :: thesis: verum

end;A10: 1 <= j and

A11: j < i and

A12: 1 <= k and

A13: k < i and

A14: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;

A15: k <= len f by A8, A13, XXREAL_0:2;

then A16: k <= len f2 by A4, NAT_1:12;

A17: f /. k = f . k by A12, A15, Lm1

.= f2 . k by A1, A12, A15, FINSEQ_1:64

.= f2 /. k by A12, A16, Lm1 ;

A18: j <= len f by A8, A11, XXREAL_0:2;

then A19: j <= len f2 by A4, NAT_1:12;

f /. j = f . j by A10, A18, Lm1

.= f2 . j by A1, A10, A18, FINSEQ_1:64

.= f2 /. j by A10, A19, Lm1 ;

hence prc f2,X,i by A9, A10, A11, A12, A13, A14, A17; :: thesis: verum

suppose
ex j being Nat st

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: prc f2,X,i

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: prc f2,X,i

then consider j being Nat such that

A20: 1 <= j and

A21: j < i and

A22: f /. j NEX_rule f /. i ;

A23: j <= len f by A8, A21, XXREAL_0:2;

then A24: j <= len f2 by A4, NAT_1:12;

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

.= f2 . j by A1, A20, A23, FINSEQ_1:64

.= f2 /. j by A20, A24, Lm1 ;

hence prc f2,X,i by A9, A20, A21, A22; :: thesis: verum

end;A20: 1 <= j and

A21: j < i and

A22: f /. j NEX_rule f /. i ;

A23: j <= len f by A8, A21, XXREAL_0:2;

then A24: j <= len f2 by A4, NAT_1:12;

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

.= f2 . j by A1, A20, A23, FINSEQ_1:64

.= f2 /. j by A20, A24, Lm1 ;

hence prc f2,X,i by A9, A20, A21, A22; :: thesis: verum

suppose A25:
(len f) + 1 <= i
; :: thesis: prc f2,X,i

set i1 = i -' (len f);

i <= (len f) + (len f1) by A1, A7, FINSEQ_1:22;

then i -' (len f) <= ((len f) + (len f1)) -' (len f) by NAT_D:42;

then A26: i -' (len f) <= len f1 by NAT_D:34;

1 <= i -' (len f) by A25, NAT_D:55;

then prc f2,X,(i -' (len f)) + (len f) by A3, A4, A5, A26, Th38;

hence prc f2,X,i by A25, NAT_D:43, NAT_D:55; :: thesis: verum

end;i <= (len f) + (len f1) by A1, A7, FINSEQ_1:22;

then i -' (len f) <= ((len f) + (len f1)) -' (len f) by NAT_D:42;

then A26: i -' (len f) <= len f1 by NAT_D:34;

1 <= i -' (len f) by A25, NAT_D:55;

then prc f2,X,(i -' (len f)) + (len f) by A3, A4, A5, A26, Th38;

hence prc f2,X,i by A25, NAT_D:43, NAT_D:55; :: thesis: verum