:: deftheorem Def21 defines the_argument_of MODELC_1:def 21 :
for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds
for b₂ being CTL-formula holds
( ( H is negative implies ( b₂ = the_argument_of H iff 'not' b₂ = H ) ) & ( H is ExistNext implies ( b₂ = the_argument_of H iff EX b₂ = H ) ) & ( not H is negative & not H is ExistNext implies ( b₂ = the_argument_of H iff EG b₂ = H ) ) );