defpred S_{1}[ Nat, set , set ] means ex A, B being Element of LTLB_WFF st

( A = $2 & B = $3 & B = (f /. ($1 + 1)) => A );

A2: ( len p = len f & ( p . 1 = (f /. 1) => A or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

S_{1}[n,p . n,p . (n + 1)] ) )
from RECDEF_1:sch 4(A1);

thus ( len f > 0 implies ex p being FinSequence of LTLB_WFF st

( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) ) ) :: thesis: ( not len f > 0 implies ex b_{1} being FinSequence of LTLB_WFF st b_{1} = <*> LTLB_WFF )_{1} being FinSequence of LTLB_WFF st b_{1} = <*> LTLB_WFF )
; :: thesis: verum

( A = $2 & B = $3 & B = (f /. ($1 + 1)) => A );

A1: now :: thesis: for n being Nat st 1 <= n & n < len f holds

for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S_{1}[n,x,y]

consider p being FinSequence of LTLB_WFF such that for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S

let n be Nat; :: thesis: ( 1 <= n & n < len f implies for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S_{1}[n,x,y] )

assume ( 1 <= n & n < len f ) ; :: thesis: for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S_{1}[n,x,y]

let x be Element of LTLB_WFF ; :: thesis: ex y being Element of LTLB_WFF st S_{1}[n,x,y]

S_{1}[n,x,(f /. (n + 1)) => x]
;

hence ex y being Element of LTLB_WFF st S_{1}[n,x,y]
; :: thesis: verum

end;assume ( 1 <= n & n < len f ) ; :: thesis: for x being Element of LTLB_WFF ex y being Element of LTLB_WFF st S

let x be Element of LTLB_WFF ; :: thesis: ex y being Element of LTLB_WFF st S

S

hence ex y being Element of LTLB_WFF st S

A2: ( len p = len f & ( p . 1 = (f /. 1) => A or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

S

thus ( len f > 0 implies ex p being FinSequence of LTLB_WFF st

( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) ) ) :: thesis: ( not len f > 0 implies ex b

proof

thus
( not len f > 0 implies ex b
assume A3:
len f > 0
; :: thesis: ex p being FinSequence of LTLB_WFF st

( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) )

take p ; :: thesis: ( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) )

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) ) by A2, A3; :: thesis: verum

end;( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) )

take p ; :: thesis: ( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) )

now :: thesis: for i being Element of NAT st 1 <= i & i < len f holds

p . (i + 1) = (f /. (i + 1)) => (p /. i)

hence
( len p = len f & p . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds p . (i + 1) = (f /. (i + 1)) => (p /. i)

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies p . (i + 1) = (f /. (i + 1)) => (p /. i) )

assume A4: ( 1 <= i & i < len f ) ; :: thesis: p . (i + 1) = (f /. (i + 1)) => (p /. i)

then ex A, B being Element of LTLB_WFF st

( A = p . i & B = p . (i + 1) & B = (f /. (i + 1)) => A ) by A2;

hence p . (i + 1) = (f /. (i + 1)) => (p /. i) by FINSEQ_4:15, A4, A2; :: thesis: verum

end;assume A4: ( 1 <= i & i < len f ) ; :: thesis: p . (i + 1) = (f /. (i + 1)) => (p /. i)

then ex A, B being Element of LTLB_WFF st

( A = p . i & B = p . (i + 1) & B = (f /. (i + 1)) => A ) by A2;

hence p . (i + 1) = (f /. (i + 1)) => (p /. i) by FINSEQ_4:15, A4, A2; :: thesis: verum

p . (i + 1) = (f /. (i + 1)) => (p /. i) ) ) by A2, A3; :: thesis: verum