:: deftheorem defines is_a_correct_step_wrt GRZLOG_1:def 29 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P being GRZ-formula-sequence
for n being Element of NAT holds
( P,n is_a_correct_step_wrt A,R iff ( P . n in A or ex Q being GRZ-formula-finset st
( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds
ex k being Element of NAT st
( k in dom P & k < n & P . k = q ) ) ) ) );