let H be LTL-formula; :: thesis: for W, W1, W2 being Subset of (Subformulae H) st W = W1 \/ W2 holds
len W <= (len W1) + (len W2)
let W, W1, W2 be Subset of (Subformulae H); :: thesis: ( W = W1 \/ W2 implies len W <= (len W1) + (len W2) )
defpred S₁[ Nat] means for W, W1, W2 being Subset of (Subformulae H) st card W1 <= $1 & W = W1 \/ W2 holds
len W <= (len W1) + (len W2);
set k = card W1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let W, W1, W2 be Subset of (Subformulae H); :: thesis: ( card W1 <= k + 1 & W = W1 \/ W2 implies len W <= (len W1) + (len W2) )
assume A3: card W1 <= k + 1 ; :: thesis: ( not W = W1 \/ W2 or len W <= (len W1) + (len W2) )
( W = W1 \/ W2 implies len W <= (len W1) + (len W2) )

proof

assume A4: W = W1 \/ W2 ; :: thesis: len W <= (len W1) + (len W2)

now :: thesis: len W <= (len W1) + (len W2)

per cases ( card W1 <= k or card W1 = k + 1 ) by A3, NAT_1:8;

suppose card W1 <= k ; :: thesis: len W <= (len W1) + (len W2)

hence len W <= (len W1) + (len W2) by A2, A4; :: thesis: verum

end;

suppose card W1 = k + 1 ; :: thesis: len W <= (len W1) + (len W2)

then W1 <> {} ;
then consider x being object such that
A5: x in W1 by XBOOLE_0:def 1;
x in Subformulae H by A5;
then reconsider x = x as LTL-formula by MODELC_2:1;
set X = {x};
set Y = W1 \ {x};
set Z = (W1 \ {x}) \/ W2;
A6: {x} c= W1 by A5, ZFMISC_1:31;
then card (W1 \ {x}) = (card W1) - (card {x}) by CARD_2:44
.= (card W1) - 1 by CARD_1:30 ;
then (card (W1 \ {x})) + 1 = card W1 ;
then card (W1 \ {x}) <= k by A3, XREAL_1:6;
then ( (W1 \ {x}) \/ W2 = (W1 \ {x}) \/ W2 implies len ((W1 \ {x}) \/ W2) <= (len (W1 \ {x})) + (len W2) ) by A2;
then len ((W1 \ {x}) \/ W2) <= ((len W1) - (len x)) + (len W2) by A5, Th10;
then len ((W1 \ {x}) \/ W2) <= ((len W1) + (len W2)) - (len x) ;
then A7: (len ((W1 \ {x}) \/ W2)) + (len x) <= (len W1) + (len W2) by XREAL_1:19;
((W1 \ {x}) \/ W2) \/ {x} = ((W1 \ {x}) \/ {x}) \/ W2 by XBOOLE_1:4
.= W1 \/ W2 by A6, XBOOLE_1:45 ;
then len W <= (len ((W1 \ {x}) \/ W2)) + (len x) by A4, Th12;
hence len W <= (len W1) + (len W2) by A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence len W <= (len W1) + (len W2) ; :: thesis: verum

end;

hence ( not W = W1 \/ W2 or len W <= (len W1) + (len W2) ) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A8: S₁[ 0 ]

proof

let W, W1, W2 be Subset of (Subformulae H); :: thesis: ( card W1 <= 0 & W = W1 \/ W2 implies len W <= (len W1) + (len W2) )
assume card W1 <= 0 ; :: thesis: ( not W = W1 \/ W2 or len W <= (len W1) + (len W2) )
then A9: W1 = {} H ;
then len W1 = 0 by Th13;
hence ( not W = W1 \/ W2 or len W <= (len W1) + (len W2) ) by A9; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A1);
then S₁[ card W1] ;
hence ( W = W1 \/ W2 implies len W <= (len W1) + (len W2) ) ; :: thesis: verum