theorem :: MODELC_2:78

for H being LTL-formula holds
( ( H is atomic implies ( not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is negative implies ( not H is atomic & not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is conjunctive implies ( not H is atomic & not H is negative & not H is disjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is disjunctive implies ( not H is atomic & not H is negative & not H is conjunctive & not H is next & not H is Until & not H is Release ) ) & ( H is next implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is Until & not H is Release ) ) & ( H is Until implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Release ) ) & ( H is Release implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until ) ) ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21;