let p, q be Element of LTLB_WFF ; :: thesis: ( p in tau1 . q & p <> q implies len p < len q )

defpred S_{1}[ Element of LTLB_WFF ] means ( p in tau1 . $1 & p <> $1 implies len p < len $1 );

A1: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r 'U' s] & S_{1}[r => s] )

then A8: S_{1}[ TFALSUM ]
by TARSKI:def 1;

for p being Element of LTLB_WFF holds S_{1}[p]
from HILBERT2:sch 2(A8, A1, A2);

hence ( p in tau1 . q & p <> q implies len p < len q ) ; :: thesis: verum

defpred S

A1: for n being Element of NAT holds S

proof

A2:
for r, s being Element of LTLB_WFF st S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

tau1 . (prop n) = {(prop n)} by Def4;

hence S_{1}[ prop n]
by TARSKI:def 1; :: thesis: verum

end;tau1 . (prop n) = {(prop n)} by Def4;

hence S

( S

proof

tau1 . TFALSUM = {TFALSUM}
by Def4;
let r, s be Element of LTLB_WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r 'U' s] & S_{1}[r => s] ) )

assume that

A3: S_{1}[r]
and

A4: S_{1}[s]
; :: thesis: ( S_{1}[r 'U' s] & S_{1}[r => s] )

set u = r => s;

tau1 . (r 'U' s) = {(r 'U' s)} by Def4;

hence S_{1}[r 'U' s]
by TARSKI:def 1; :: thesis: S_{1}[r => s]

thus S_{1}[r => s]
:: thesis: verum

end;assume that

A3: S

A4: S

set u = r => s;

tau1 . (r 'U' s) = {(r 'U' s)} by Def4;

hence S

thus S

proof

assume that

A5: p in tau1 . (r => s) and

A6: p <> r => s ; :: thesis: len p < len (r => s)

tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;

then p in {(r => s)} \/ ((tau1 . r) \/ (tau1 . s)) by XBOOLE_1:4, A5;

then A7: ( p in {(r => s)} or p in (tau1 . r) \/ (tau1 . s) ) by XBOOLE_0:def 3;

end;A5: p in tau1 . (r => s) and

A6: p <> r => s ; :: thesis: len p < len (r => s)

tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;

then p in {(r => s)} \/ ((tau1 . r) \/ (tau1 . s)) by XBOOLE_1:4, A5;

then A7: ( p in {(r => s)} or p in (tau1 . r) \/ (tau1 . s) ) by XBOOLE_0:def 3;

then A8: S

for p being Element of LTLB_WFF holds S

hence ( p in tau1 . q & p <> q implies len p < len q ) ; :: thesis: verum