let f, g be FinSequence of CQC-WFF ; :: thesis: ( Ant f = Ant g & |- f & |- g implies |- (Ant f) ^ <*((Suc f) '&' (Suc g))*> )
assume A1:
( Ant f = Ant g & |- f & |- g )
; :: thesis: |- (Ant f) ^ <*((Suc f) '&' (Suc g))*>
then consider PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] such that
A2:
( PR is a_proof & f = (PR . (len PR)) `1 )
by Def9;
consider PR1 being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] such that
A3:
( PR1 is a_proof & g = (PR1 . (len PR1)) `1 )
by A1, Def9;
A4:
( (Ant f) ^ <*((Suc f) '&' (Suc g))*> in set_of_CQC-WFF-seq & 5 in Proof_Step_Kinds )
by Def6, CQC_THE1:43;
then
rng <*[((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]*> c= [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :]
by TARSKI:def 3;
then reconsider PR2 = <*[((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]*> as FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] by FINSEQ_1:def 4;
set PR3 = (PR ^ PR1) ^ PR2;
reconsider PR3 = (PR ^ PR1) ^ PR2 as FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] ;
A6:
PR <> {}
by A2, Def8;
then A7:
PR ^ PR1 <> {}
;
now let n be
Nat;
:: thesis: ( 1 <= n & n <= len PR3 implies PR3,n is_a_correct_step )assume A9:
( 1
<= n &
n <= len PR3 )
;
:: thesis: PR3,n is_a_correct_step A10:
n in dom PR3
by A9, FINSEQ_3:27;
A11:
now assume A12:
n in dom (PR ^ PR1)
;
:: thesis: PR3,n is_a_correct_step now given k being
Nat such that A16:
(
k in dom PR1 &
n = (len PR) + k )
;
:: thesis: PR3,n is_a_correct_step A17:
( 1
<= k &
k <= len PR1 )
by A16, FINSEQ_3:27;
then
PR1,
k is_a_correct_step
by A3, Def8;
then A18:
PR ^ PR1,
n is_a_correct_step
by A16, A17, Th35;
A19:
n <= (len PR1) + (len PR)
by A16, A17, XREAL_1:8;
k <= n
by A16, NAT_1:11;
then
( 1
<= n &
n <= len (PR ^ PR1) )
by A17, A19, FINSEQ_1:35, XXREAL_0:2;
hence
PR3,
n is_a_correct_step
by A18, Th34;
:: thesis: verum end; hence
PR3,
n is_a_correct_step
by A12, A13, FINSEQ_1:38;
:: thesis: verum end; now given k being
Nat such that A20:
(
k in dom PR2 &
n = (len (PR ^ PR1)) + k )
;
:: thesis: PR3,n is_a_correct_step
k in Seg 1
by A20, FINSEQ_1:55;
then A21:
k = 1
by FINSEQ_1:4, TARSKI:def 1;
then
PR2 . k = [((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]
by FINSEQ_1:57;
then
(
(PR2 . k) `1 = (Ant f) ^ <*((Suc f) '&' (Suc g))*> &
(PR2 . k) `2 = 5 )
by MCART_1:7;
then A22:
(
(PR3 . n) `1 = (Ant f) ^ <*((Suc f) '&' (Suc g))*> &
(PR3 . n) `2 = 5 )
by A20, FINSEQ_1:def 7;
A23:
PR1 <> {}
by A3, Def8;
then A24:
( 1
<= len PR &
len PR < len (PR ^ PR1) )
by A6, Th6;
then
len PR in dom PR
by FINSEQ_3:27;
then A25:
f = ((PR ^ PR1) . (len PR)) `1
by A2, FINSEQ_1:def 7;
len PR in dom (PR ^ PR1)
by A24, FINSEQ_3:27;
then A26:
f = (PR3 . (len PR)) `1
by A25, FINSEQ_1:def 7;
A27:
( 1
<= len (PR ^ PR1) &
len (PR ^ PR1) < n )
by A7, A20, A21, Th6, NAT_1:13;
1
<= len PR1
by A23, Th6;
then
len PR1 in dom PR1
by FINSEQ_3:27;
then
g = ((PR ^ PR1) . ((len PR) + (len PR1))) `1
by A3, FINSEQ_1:def 7;
then A28:
g = ((PR ^ PR1) . (len (PR ^ PR1))) `1
by FINSEQ_1:35;
1
<= len (PR ^ PR1)
by A7, Th6;
then
len (PR ^ PR1) in dom (PR ^ PR1)
by FINSEQ_3:27;
then
g = (PR3 . (len (PR ^ PR1))) `1
by A28, FINSEQ_1:def 7;
hence
PR3,
n is_a_correct_step
by A1, A22, A24, A26, A27, Def7;
:: thesis: verum end; hence
PR3,
n is_a_correct_step
by A10, A11, FINSEQ_1:38;
:: thesis: verum end;
then A29:
PR3 is a_proof
by Def8;
PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + (len PR2))
by FINSEQ_1:35;
then A30:
PR3 . (len PR3) = PR3 . ((len (PR ^ PR1)) + 1)
by FINSEQ_1:56;
1 in Seg 1
by FINSEQ_1:4, TARSKI:def 1;
then
1 in dom PR2
by FINSEQ_1:55;
then
PR3 . (len PR3) = PR2 . 1
by A30, FINSEQ_1:def 7;
then
PR3 . (len PR3) = [((Ant f) ^ <*((Suc f) '&' (Suc g))*>),5]
by FINSEQ_1:57;
then
(PR3 . (len PR3)) `1 = (Ant f) ^ <*((Suc f) '&' (Suc g))*>
by MCART_1:7;
hence
|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>
by A29, Def9; :: thesis: verum