let A be non empty Subset of GRZ-formula-set; for R being GRZ-rule
for t being GRZ-formula
for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
let R be GRZ-rule; for t being GRZ-formula
for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
let t be GRZ-formula; for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
let S be GRZ-formula-finset; ( A,R |- S & [S,t] in R implies A,R |- t )
assume that
A1:
A,R |- S
and
A2:
[S,t] in R
; A,R |- t
consider S1 being GRZ-formula-finset such that
A3:
S c= S1
and
A4:
S1 is A,R -correct
by A1, Th47;
consider P1 being GRZ-formula-sequence such that
A5:
S1 = rng P1
and
A6:
P1 is A,R -correct
by A4;
set P2 = P1 ^ <*t*>;
(rng P1) \/ (rng <*t*>) c= GRZ-formula-set
by XBOOLE_1:8;
then
rng (P1 ^ <*t*>) c= GRZ-formula-set
by FINSEQ_1:31;
then reconsider P2 = P1 ^ <*t*> as GRZ-formula-sequence by FINSEQ_1:def 4;
take
P2
; GRZLOG_1:def 32 ( t in rng P2 & P2 is A,R -correct )
rng <*t*> = {t}
by FINSEQ_1:38;
then
t in rng <*t*>
by TARSKI:def 1;
then
t in (rng P1) \/ (rng <*t*>)
by XBOOLE_0:def 3;
hence
t in rng P2
by FINSEQ_1:31; P2 is A,R -correct
let k be Element of NAT ; GRZLOG_1:def 30 ( k in dom P2 implies P2,k is_a_correct_step_wrt A,R )
reconsider j = k as Nat ;
assume
k in dom P2
; P2,k is_a_correct_step_wrt A,R