let A be non empty Subset of GRZ-formula-set; for R being GRZ-rule
for P1, P2 being GRZ-formula-sequence st P1 is A,R -correct & P2 is A,R -correct holds
P1 ^ P2 is A,R -correct
let R be GRZ-rule; for P1, P2 being GRZ-formula-sequence st P1 is A,R -correct & P2 is A,R -correct holds
P1 ^ P2 is A,R -correct
let P1, P2 be GRZ-formula-sequence; ( P1 is A,R -correct & P2 is A,R -correct implies P1 ^ P2 is A,R -correct )
set P0 = <*> GRZ-formula-set;
assume that
A1:
P1 is A,R -correct
and
A2:
P2 is A,R -correct
; P1 ^ P2 is A,R -correct
let k be Element of NAT ; GRZLOG_1:def 30 ( k in dom (P1 ^ P2) implies P1 ^ P2,k is_a_correct_step_wrt A,R )
assume A3:
k in dom (P1 ^ P2)
; P1 ^ P2,k is_a_correct_step_wrt A,R
per cases
( k in dom P1 or (P1 ^ P2) . k in A or ( not k in dom P1 & not (P1 ^ P2) . k in A ) )
;
suppose that A10:
not
k in dom P1
and A11:
not
(P1 ^ P2) . k in A
;
P1 ^ P2,k is_a_correct_step_wrt A,Rconsider j being
Nat such that A12:
j in dom P2
and A13:
k = (len P1) + j
by A3, A10, FINSEQ_1:25;
reconsider m =
j as
Element of
NAT by ORDINAL1:def 12;
A15:
P2,
m is_a_correct_step_wrt A,
R
by A2, A12;
A16:
(P1 ^ P2) . k = P2 . m
by A12, A13, FINSEQ_1:def 7;
then consider Q being
GRZ-formula-finset such that A20:
[Q,(P2 . m)] in R
and A21:
for
q being
FinSequence st
q in Q holds
ex
i being
Element of
NAT st
(
i in dom P2 &
i < m &
P2 . i = q )
by A11, A15;
for
q being
FinSequence st
q in Q holds
ex
u being
Element of
NAT st
(
u in dom (P1 ^ P2) &
u < k &
(P1 ^ P2) . u = q )
hence
P1 ^ P2,
k is_a_correct_step_wrt A,
R
by A16, A20;
verum end; end;