let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for P, P1, P2 being GRZ-formula-sequence st P is A,R -correct & P = P1 ^ P2 holds
P1 is A,R -correct
let R be GRZ-rule; :: thesis: for P, P1, P2 being GRZ-formula-sequence st P is A,R -correct & P = P1 ^ P2 holds
P1 is A,R -correct
let P, P1, P2 be GRZ-formula-sequence; :: thesis: ( P is A,R -correct & P = P1 ^ P2 implies P1 is A,R -correct )
assume that
A1: P is A,R -correct and
A2: P = P1 ^ P2 ; :: thesis: P1 is A,R -correct
set P0 = <*> GRZ-formula-set;
let k be Element of NAT ; :: according to GRZLOG_1:def 30 :: thesis: ( k in dom P1 implies P1,k is_a_correct_step_wrt A,R )
assume A3: k in dom P1 ; :: thesis: P1,k is_a_correct_step_wrt A,R
dom P1 c= dom P by A2, FINSEQ_1:26;
then P1 ^ (<*> GRZ-formula-set),k is_a_correct_step_wrt A,R by A1, A2, A3, Lm41;
hence P1,k is_a_correct_step_wrt A,R by FINSEQ_1:34; :: thesis: verum