let Al be QC-alphabet ; 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; 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:]; ( 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
; 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 )
;
CALCUL_1:def 7case
((PR ^ PR1) . (n + (len PR))) `2 = 2
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 3
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 4
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 5
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 6
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 7
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 8
;
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;
verum end; case
((PR ^ PR1) . (n + (len PR))) `2 = 9
;
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;
verum end; end;