B1: ( H is conjunctive implies ex G, H1 being LTL-formula st H1 '&' G = H )

proof

assume H is conjunctive ; :: thesis: ex G, H1 being LTL-formula st H1 '&' G = H
then consider G, F being LTL-formula such that
C1: G '&' F = H by Def16;
take F ; :: thesis: ex H1 being LTL-formula st H1 '&' F = H
thus ex H1 being LTL-formula st H1 '&' F = H by C1; :: thesis: verum

end;

B2: ( H is disjunctive implies ex G, H1 being LTL-formula st H1 'or' G = H )

proof

assume H is disjunctive ; :: thesis: ex G, H1 being LTL-formula st H1 'or' G = H
then consider G, F being LTL-formula such that
C1: G 'or' F = H by Def17;
take F ; :: thesis: ex H1 being LTL-formula st H1 'or' F = H
thus ex H1 being LTL-formula st H1 'or' F = H by C1; :: thesis: verum

end;

B3: ( H is Until implies ex G, H1 being LTL-formula st H1 'U' G = H )

proof

assume H is Until ; :: thesis: ex G, H1 being LTL-formula st H1 'U' G = H
then consider G, F being LTL-formula such that
C1: G 'U' F = H by Def19;
take F ; :: thesis: ex H1 being LTL-formula st H1 'U' F = H
thus ex H1 being LTL-formula st H1 'U' F = H by C1; :: thesis: verum

end;

( not H is conjunctive & not H is disjunctive & not H is Until implies ex G, H1 being LTL-formula st H1 'R' G = H )

proof

assume ( not H is conjunctive & not H is disjunctive & not H is Until ) ; :: thesis: ex G, H1 being LTL-formula st H1 'R' G = H
then consider G, F being LTL-formula such that
C2: G 'R' F = H by Def1901, A1;
take F ; :: thesis: ex H1 being LTL-formula st H1 'R' F = H
thus ex H1 being LTL-formula st H1 'R' F = H by C2; :: thesis: verum

end;

hence ( ( H is conjunctive implies ex b₁, H1 being LTL-formula st H1 '&' b₁ = H ) & ( H is disjunctive implies ex b₁, H1 being LTL-formula st H1 'or' b₁ = H ) & ( H is Until implies ex b₁, H1 being LTL-formula st H1 'U' b₁ = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b₁, H1 being LTL-formula st H1 'R' b₁ = H ) ) by B1, B2, B3; :: thesis: verum