scheme :: MODELC_2:sch 1
LTLInd{ P₁[ LTL-formula] } :

for H being LTL-formula holds P₁[H]

provided

A1: for H being LTL-formula st H is atomic holds
P₁[H] and
A2: for H being LTL-formula st ( H is negative or H is next ) & P₁[ the_argument_of H] holds
P₁[H] and
A3: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & P₁[ the_left_argument_of H] & P₁[ the_right_argument_of H] holds
P₁[H]