let Al be QC-alphabet ; for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & |- f & |- g holds
|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>
let f, g be FinSequence of CQC-WFF Al; ( Ant f = Ant g & |- f & |- g implies |- (Ant f) ^ <*((Suc f) '&' (Suc g))*> )
assume that
A1:
Ant f = Ant g
and
A2:
|- f
and
A3:
|- g
; |- (Ant f) ^ <*((Suc f) '&' (Suc g))*>
consider PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A4:
PR1 is a_proof
and
A5:
g = (PR1 . (len PR1)) `1
by A3;
consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A6:
PR is a_proof
and
A7:
f = (PR . (len PR)) `1
by A2;
A8:
(Ant f) ^ <*((Suc f) '&' (Suc g))*> in set_of_CQC-WFF-seq Al
by Def6;
then
rng <*[((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
;
then reconsider PR2 = <*[((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1
by FINSEQ_1:2, TARSKI:def 1;
then A9:
1 in dom PR2
by FINSEQ_1:38;
set PR3 = (PR ^ PR1) ^ PR2;
reconsider PR3 = (PR ^ PR1) ^ PR2 as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ;
A10:
PR <> {}
by A6;
now for n being Nat st 1 <= n & n <= len PR3 holds
PR3,n is_a_correct_step let n be
Nat;
( 1 <= n & n <= len PR3 implies PR3,n is_a_correct_step )assume
( 1
<= n &
n <= len PR3 )
;
PR3,n is_a_correct_step then A11:
n in dom PR3
by FINSEQ_3:25;
A12:
now ( ex k being Nat st
( k in dom PR2 & n = (len (PR ^ PR1)) + k ) implies PR3,n is_a_correct_step )given k being
Nat such that A13:
k in dom PR2
and A14:
n = (len (PR ^ PR1)) + k
;
PR3,n is_a_correct_step
k in Seg 1
by A13, FINSEQ_1:38;
then A15:
k = 1
by FINSEQ_1:2, TARSKI:def 1;
then A16:
PR2 . k = [((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]
by FINSEQ_1:40;
then
(PR2 . k) `1 = (Ant f) ^ <*((Suc f) '&' (Suc g))*>
;
then A17:
(PR3 . n) `1 = (Ant f) ^ <*((Suc f) '&' (Suc g))*>
by A13, A14, FINSEQ_1:def 7;
(PR2 . k) `2 = 5
by A16;
then A18:
(PR3 . n) `2 = 5
by A13, A14, FINSEQ_1:def 7;
A19:
len (PR ^ PR1) < n
by A14, A15, NAT_1:13;
A20:
1
<= len PR
by A10, Th6;
then
len PR in dom PR
by FINSEQ_3:25;
then A21:
f = ((PR ^ PR1) . (len PR)) `1
by A7, FINSEQ_1:def 7;
A22:
PR1 <> {}
by A4;
then A23:
len PR < len (PR ^ PR1)
by Th6;
then
len PR in dom (PR ^ PR1)
by A20, FINSEQ_3:25;
then A24:
f = (PR3 . (len PR)) `1
by A21, FINSEQ_1:def 7;
1
<= len PR1
by A22, Th6;
then
len PR1 in dom PR1
by FINSEQ_3:25;
then
g = ((PR ^ PR1) . ((len PR) + (len PR1))) `1
by A5, FINSEQ_1:def 7;
then A25:
g = ((PR ^ PR1) . (len (PR ^ PR1))) `1
by FINSEQ_1:22;
1
<= len (PR ^ PR1)
by A10, Th6;
then
len (PR ^ PR1) in dom (PR ^ PR1)
by FINSEQ_3:25;
then A26:
g = (PR3 . (len (PR ^ PR1))) `1
by A25, FINSEQ_1:def 7;
1
<= len (PR ^ PR1)
by A10, Th6;
hence
PR3,
n is_a_correct_step
by A1, A17, A18, A20, A23, A24, A19, A26, Def7;
verum end; now ( n in dom (PR ^ PR1) implies PR3,n is_a_correct_step )A27:
now ( ex k being Nat st
( k in dom PR1 & n = (len PR) + k ) implies PR3,n is_a_correct_step )given k being
Nat such that A28:
k in dom PR1
and A29:
n = (len PR) + k
;
PR3,n is_a_correct_step A30:
1
<= k
by A28, FINSEQ_3:25;
A31:
k <= len PR1
by A28, FINSEQ_3:25;
then
n <= (len PR1) + (len PR)
by A29, XREAL_1:6;
then A32:
n <= len (PR ^ PR1)
by FINSEQ_1:22;
k <= n
by A29, NAT_1:11;
then A33:
1
<= n
by A30, XXREAL_0:2;
PR1,
k is_a_correct_step
by A4, A30, A31;
then
PR ^ PR1,
n is_a_correct_step
by A29, A30, A31, Th35;
hence
PR3,
n is_a_correct_step
by A33, A32, Th34;
verum end; A34:
now ( n in dom PR implies PR3,n is_a_correct_step )assume A35:
n in dom PR
;
PR3,n is_a_correct_step then A36:
1
<= n
by FINSEQ_3:25;
A37:
n <= len PR
by A35, FINSEQ_3:25;
len PR <= len (PR ^ PR1)
by Th6;
then A38:
n <= len (PR ^ PR1)
by A37, XXREAL_0:2;
PR,
n is_a_correct_step
by A6, A36, A37;
then
PR ^ PR1,
n is_a_correct_step
by A36, A37, Th34;
hence
PR3,
n is_a_correct_step
by A36, A38, Th34;
verum end; assume
n in dom (PR ^ PR1)
;
PR3,n is_a_correct_step hence
PR3,
n is_a_correct_step
by A34, A27, FINSEQ_1:25;
verum end; hence
PR3,
n is_a_correct_step
by A11, A12, FINSEQ_1:25;
verum end;
then A39:
PR3 is a_proof
;
PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + (len PR2))
by FINSEQ_1:22;
then
PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + 1)
by FINSEQ_1:39;
then
PR3 . (len PR3) = PR2 . 1
by A9, FINSEQ_1:def 7;
then
PR3 . (len PR3) = [((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]
by FINSEQ_1:40;
then
(PR3 . (len PR3)) `1 = (Ant f) ^ <*((Suc f) '&' (Suc g))*>
;
hence
|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>
by A39; verum