let H be LTL-formula; :: thesis: ex L being FinSequence st Subformulae H = rng L
defpred S1[ LTL-formula] means ex L being FinSequence st Subformulae $1 = rng L;
A1: for H being LTL-formula st ( H is negative or H is next ) & S1[ the_argument_of H] holds
S1[H]
proof
let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) & S1[ the_argument_of H] implies S1[H] )
assume that
A2: ( H is negative or H is next ) and
A3: S1[ the_argument_of H] ; :: thesis: S1[H]
consider L1 being FinSequence such that
A4: Subformulae (the_argument_of H) = rng L1 by A3;
set L = L1 ^ <*H*>;
take L1 ^ <*H*> ; :: thesis: Subformulae H = rng (L1 ^ <*H*>)
rng (L1 ^ <*H*>) = (rng L1) \/ (rng <*H*>) by FINSEQ_1:31
.= (Subformulae (the_argument_of H)) \/ {H} by A4, Lm3
.= Subformulae H by A2, Lm21 ;
hence Subformulae H = rng (L1 ^ <*H*>) ; :: thesis: verum
end;
A5: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds
S1[H]
proof
let H be LTL-formula; :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] )
assume that
A6: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) and
A7: S1[ the_left_argument_of H] and
A8: S1[ the_right_argument_of H] ; :: thesis: S1[H]
consider L1 being FinSequence such that
A9: Subformulae (the_left_argument_of H) = rng L1 by A7;
consider L2 being FinSequence such that
A10: Subformulae (the_right_argument_of H) = rng L2 by A8;
A11: rng (L1 ^ L2) = (Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H)) by A9, A10, FINSEQ_1:31;
set L = (L1 ^ L2) ^ <*H*>;
take (L1 ^ L2) ^ <*H*> ; :: thesis: Subformulae H = rng ((L1 ^ L2) ^ <*H*>)
rng ((L1 ^ L2) ^ <*H*>) = (rng (L1 ^ L2)) \/ (rng <*H*>) by FINSEQ_1:31
.= ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by A11, Lm3
.= Subformulae H by A6, Lm22 ;
hence Subformulae H = rng ((L1 ^ L2) ^ <*H*>) ; :: thesis: verum
end;
A12: for H being LTL-formula st H is atomic holds
S1[H]
proof
let H be LTL-formula; :: thesis: ( H is atomic implies S1[H] )
assume A13: H is atomic ; :: thesis: S1[H]
set L = <*H*>;
take <*H*> ; :: thesis: Subformulae H = rng <*H*>
rng <*H*> = {H} by Lm3
.= Subformulae H by A13, Lm23 ;
hence Subformulae H = rng <*H*> ; :: thesis: verum
end;
for H being LTL-formula holds S1[H] from MODELC_2:sch 1(A12, A1, A5);
 hence ex L being FinSequence st Subformulae H = rng L ; :: thesis: verum