let Al be QC-alphabet ; :: thesis: for n being Nat
for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR1 & PR1,n is_a_correct_step holds
PR ^ PR1,n + (len PR) is_a_correct_step
let n be Nat; :: thesis: for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR1 & PR1,n is_a_correct_step holds
PR ^ PR1,n + (len PR) is_a_correct_step
let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; :: thesis: ( 1 <= n & n <= len PR1 & PR1,n is_a_correct_step implies PR ^ PR1,n + (len PR) is_a_correct_step )
assume that
A1: 1 <= n and
A2: n <= len PR1 and
A3: PR1,n is_a_correct_step ; :: thesis: PR ^ PR1,n + (len PR) is_a_correct_step
n in dom PR1 by A1, A2, FINSEQ_3:25;
then A4: PR1 . n = (PR ^ PR1) . (n + (len PR)) by FINSEQ_1:def 7;
n + (len PR) <= (len PR) + (len PR1) by A2, XREAL_1:6;
then A5: n + (len PR) <= len (PR ^ PR1) by FINSEQ_1:22;
not not ((PR ^ PR1) . (n + (len PR))) `2 = 0 & ... & not ((PR ^ PR1) . (n + (len PR))) `2 = 9 by A1, A5, Th31, NAT_1:12;
per cases then ( ((PR ^ PR1) . (n + (len PR))) `2 = 0 or ((PR ^ PR1) . (n + (len PR))) `2 = 1 or ((PR ^ PR1) . (n + (len PR))) `2 = 2 or ((PR ^ PR1) . (n + (len PR))) `2 = 3 or ((PR ^ PR1) . (n + (len PR))) `2 = 4 or ((PR ^ PR1) . (n + (len PR))) `2 = 5 or ((PR ^ PR1) . (n + (len PR))) `2 = 6 or ((PR ^ PR1) . (n + (len PR))) `2 = 7 or ((PR ^ PR1) . (n + (len PR))) `2 = 8 or ((PR ^ PR1) . (n + (len PR))) `2 = 9 ) ;
:: according to CALCUL_1:def 7
case ((PR ^ PR1) . (n + (len PR))) `2 = 0 ; :: thesis: ex f being FinSequence of CQC-WFF Al st
( Suc f is_tail_of Ant f & ((PR ^ PR1) . (n + (len PR))) `1 = f )
hence ex f being FinSequence of CQC-WFF Al st
( Suc f is_tail_of Ant f & ((PR ^ PR1) . (n + (len PR))) `1 = f ) by A3, A4, Def7; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 1 ; :: thesis: ex f being FinSequence of CQC-WFF Al st ((PR ^ PR1) . (n + (len PR))) `1 = f ^ <*(VERUM Al)*>
hence ex f being FinSequence of CQC-WFF Al st ((PR ^ PR1) . (n + (len PR))) `1 = f ^ <*(VERUM Al)*> by A3, A4, Def7; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 2 ; :: thesis: ex i being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `1 = g )
then consider i being Nat, f, g being FinSequence of CQC-WFF Al such that
A6: 1 <= i and
A7: i < n and
A8: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR1 . i) `1 = f & (PR1 . n) `1 = g ) by A3, A4, Def7;
i <= len PR1 by A2, A7, XXREAL_0:2;
then i in dom PR1 by A6, FINSEQ_3:25;
then A9: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A6, A7, NAT_1:12, XREAL_1:6;
hence ex i being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . (n + (len PR))) `1 = g ) by A4, A8, A9; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 3 ; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A10: 1 <= i and
A11: i < n and
A12: 1 <= j and
A13: j < i and
A14: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = (PR1 . j) `1 & f1 = (PR1 . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR1 . n) `1 ) by A3, A4, Def7;
A15: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A12, A13, NAT_1:12, XREAL_1:6;
A16: i <= len PR1 by A2, A11, XXREAL_0:2;
then i in dom PR1 by A10, FINSEQ_3:25;
then A17: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
j <= len PR1 by A13, A16, XXREAL_0:2;
then j in dom PR1 by A12, FINSEQ_3:25;
then A18: PR1 . j = (PR ^ PR1) . ((len PR) + j) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A10, A11, NAT_1:12, XREAL_1:6;
hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A14, A15, A17, A18; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 4 ; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that
A19: 1 <= i and
A20: i < n and
A21: 1 <= j and
A22: j < i and
A23: ( len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR1 . j) `1 & g = (PR1 . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR1 . n) `1 ) by A3, A4, Def7;
A24: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A21, A22, NAT_1:12, XREAL_1:6;
A25: i <= len PR1 by A2, A20, XXREAL_0:2;
then i in dom PR1 by A19, FINSEQ_3:25;
then A26: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
j <= len PR1 by A22, A25, XXREAL_0:2;
then j in dom PR1 by A21, FINSEQ_3:25;
then A27: PR1 . j = (PR ^ PR1) . ((len PR) + j) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A19, A20, NAT_1:12, XREAL_1:6;
hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant (Ant f)) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A23, A24, A26, A27; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 5 ; :: thesis: ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i, j being Nat, f, g being FinSequence of CQC-WFF Al such that
A28: 1 <= i and
A29: i < n and
A30: 1 <= j and
A31: j < i and
A32: ( Ant f = Ant g & f = (PR1 . j) `1 & g = (PR1 . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR1 . n) `1 ) by A3, A4, Def7;
A33: ( 1 <= (len PR) + j & (len PR) + j < i + (len PR) ) by A30, A31, NAT_1:12, XREAL_1:6;
A34: i <= len PR1 by A2, A29, XXREAL_0:2;
then i in dom PR1 by A28, FINSEQ_3:25;
then A35: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
j <= len PR1 by A31, A34, XXREAL_0:2;
then j in dom PR1 by A30, FINSEQ_3:25;
then A36: PR1 . j = (PR ^ PR1) . ((len PR) + j) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A28, A29, NAT_1:12, XREAL_1:6;
hence ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & 1 <= j & j < i & Ant f = Ant g & f = ((PR ^ PR1) . j) `1 & g = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A32, A33, A35, A36; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 6 ; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A37: 1 <= i and
A38: i < n and
A39: ( p '&' q = Suc f & f = (PR1 . i) `1 & (Ant f) ^ <*p*> = (PR1 . n) `1 ) by A3, A4, Def7;
i <= len PR1 by A2, A38, XXREAL_0:2;
then i in dom PR1 by A37, FINSEQ_3:25;
then A40: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A37, A38, NAT_1:12, XREAL_1:6;
hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A39, A40; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 7 ; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A41: 1 <= i and
A42: i < n and
A43: ( p '&' q = Suc f & f = (PR1 . i) `1 & (Ant f) ^ <*q*> = (PR1 . n) `1 ) by A3, A4, Def7;
i <= len PR1 by A2, A42, XXREAL_0:2;
then i in dom PR1 by A41, FINSEQ_3:25;
then A44: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A41, A42, NAT_1:12, XREAL_1:6;
hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st
( 1 <= i & i < n + (len PR) & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A43, A44; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 8 ; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st
( 1 <= i & i < n + (len PR) & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A45: 1 <= i and
A46: i < n and
A47: ( Suc f = All (x,p) & f = (PR1 . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR1 . n) `1 ) by A3, A4, Def7;
i <= len PR1 by A2, A46, XXREAL_0:2;
then i in dom PR1 by A45, FINSEQ_3:25;
then A48: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A45, A46, NAT_1:12, XREAL_1:6;
hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st
( 1 <= i & i < n + (len PR) & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A47, A48; :: thesis: verum
end;
case ((PR ^ PR1) . (n + (len PR))) `2 = 9 ; :: thesis: ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st
( 1 <= i & i < n + (len PR) & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . (n + (len PR))) `1 )
then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A49: 1 <= i and
A50: i < n and
A51: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR1 . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR1 . n) `1 ) by A3, A4, Def7;
i <= len PR1 by A2, A50, XXREAL_0:2;
then i in dom PR1 by A49, FINSEQ_3:25;
then A52: PR1 . i = (PR ^ PR1) . ((len PR) + i) by FINSEQ_1:def 7;
( 1 <= (len PR) + i & (len PR) + i < n + (len PR) ) by A49, A50, NAT_1:12, XREAL_1:6;
hence ex i being Nat ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st
( 1 <= i & i < n + (len PR) & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(All (x,p))*> = ((PR ^ PR1) . (n + (len PR))) `1 ) by A4, A51, A52; :: thesis: verum
end;
end;