let Al be QC-alphabet ; for f, g being FinSequence of CQC-WFF Al st 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g holds
|- (Ant (Ant f)) ^ <*(Suc f)*>
let f, g be FinSequence of CQC-WFF Al; ( 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g implies |- (Ant (Ant f)) ^ <*(Suc f)*> )
assume that
A1:
( 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g )
and
A2:
|- f
and
A3:
|- g
; |- (Ant (Ant f)) ^ <*(Suc f)*>
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 (Ant f)) ^ <*(Suc f)*> in set_of_CQC-WFF-seq Al
by Def6;
then
rng <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
;
then reconsider PR2 = <*[((Ant (Ant f)) ^ <*(Suc f)*>),3]*> 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 (Ant f)) ^ <*(Suc f)*>),3]
by FINSEQ_1:40;
then
(PR2 . k) `1 = (Ant (Ant f)) ^ <*(Suc f)*>
;
then A17:
(PR3 . n) `1 = (Ant (Ant f)) ^ <*(Suc f)*>
by A13, A14, FINSEQ_1:def 7;
(PR2 . k) `2 = 3
by A16;
then A18:
(PR3 . n) `2 = 3
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 (Ant f)) ^ <*(Suc f)*>),3]
by FINSEQ_1:40;
then
(PR3 . (len PR3)) `1 = (Ant (Ant f)) ^ <*(Suc f)*>
;
hence
|- (Ant (Ant f)) ^ <*(Suc f)*>
by A39; verum