let p, q be Element of LTLB_WFF ; :: thesis: ( p in tau1 . q & p <> q implies len p < len q )
defpred S1[ Element of LTLB_WFF ] means ( p in tau1 . \$1 & p <> \$1 implies len p < len \$1 );
A1: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
tau1 . (prop n) = {(prop n)} by Def4;
hence S1[ prop n] by TARSKI:def 1; :: thesis: verum
end;
A2: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r 'U' s] & S1[r => s] ) )
assume that
A3: S1[r] and
A4: S1[s] ; :: thesis: ( S1[r 'U' s] & S1[r => s] )
set u = r => s;
tau1 . (r 'U' s) = {(r 'U' s)} by Def4;
hence S1[r 'U' s] by TARSKI:def 1; :: thesis: S1[r => s]
thus S1[r => s] :: thesis: verum
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)} \/ ()) \/ () by Def4;
then p in {(r => s)} \/ (() \/ ()) by ;
then A7: ( p in {(r => s)} or p in () \/ () ) by XBOOLE_0:def 3;
per cases ( p in tau1 . r or p in tau1 . s ) by ;
suppose p in tau1 . r ; :: thesis: len p < len (r => s)
hence len p < len (r => s) by ; :: thesis: verum
end;
suppose p in tau1 . s ; :: thesis: len p < len (r => s)
hence len p < len (r => s) by ; :: thesis: verum
end;
end;
end;
end;
tau1 . TFALSUM = by Def4;
then A8: S1[ TFALSUM ] by TARSKI:def 1;
for p being Element of LTLB_WFF holds S1[p] from HILBERT2:sch 2(A8, A1, A2);
hence ( p in tau1 . q & p <> q implies len p < len q ) ; :: thesis: verum