let Al be QC-alphabet ; for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len PR holds
( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )
let PR, PR1 be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; for n being Nat st 1 <= n & n <= len PR holds
( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )
let n be Nat; ( 1 <= n & n <= len PR implies ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step ) )
assume that
A1:
1 <= n
and
A2:
n <= len PR
; ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step )
n in dom PR
by A1, A2, FINSEQ_3:25;
then A3:
(PR ^ PR1) . n = PR . n
by FINSEQ_1:def 7;
len (PR ^ PR1) = (len PR) + (len PR1)
by FINSEQ_1:22;
then
len PR <= len (PR ^ PR1)
by NAT_1:11;
then A4:
n <= len (PR ^ PR1)
by A2, XXREAL_0:2;
thus
( PR,n is_a_correct_step implies PR ^ PR1,n is_a_correct_step )
( PR ^ PR1,n is_a_correct_step implies PR,n is_a_correct_step )proof
assume A5:
PR,
n is_a_correct_step
;
PR ^ PR1,n is_a_correct_step
not not
((PR ^ PR1) . n) `2 = 0 & ... & not
((PR ^ PR1) . n) `2 = 9
by A1, A4, Th31;
per cases then
( ((PR ^ PR1) . n) `2 = 0 or ((PR ^ PR1) . n) `2 = 1 or ((PR ^ PR1) . n) `2 = 2 or ((PR ^ PR1) . n) `2 = 3 or ((PR ^ PR1) . n) `2 = 4 or ((PR ^ PR1) . n) `2 = 5 or ((PR ^ PR1) . n) `2 = 6 or ((PR ^ PR1) . n) `2 = 7 or ((PR ^ PR1) . n) `2 = 8 or ((PR ^ PR1) . n) `2 = 9 )
;
CALCUL_1:def 7case
((PR ^ PR1) . n) `2 = 2
;
ex i being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & ((PR ^ PR1) . i) `1 = f & ((PR ^ PR1) . n) `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 &
(PR . i) `1 = f &
(PR . n) `1 = g )
by A3, A5, Def7;
i <= len PR
by A2, A7, XXREAL_0:2;
then
i in dom PR
by A6, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
hence
ex
i being
Nat ex
f,
g being
FinSequence of
CQC-WFF Al st
( 1
<= i &
i < n &
Ant f is_Subsequence_of Ant g &
Suc f = Suc g &
((PR ^ PR1) . i) `1 = f &
((PR ^ PR1) . n) `1 = g )
by A3, A6, A7, A8;
verum end; case
((PR ^ PR1) . n) `2 = 3
;
ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n & 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) `1 )then consider i,
j being
Nat,
f,
g being
FinSequence of
CQC-WFF Al such that A9:
1
<= i
and A10:
i < n
and A11:
1
<= j
and A12:
j < i
and A13:
(
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 . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 )
by A3, A5, Def7;
A14:
i <= len PR
by A2, A10, XXREAL_0:2;
then
i in Seg (len PR)
by A9, FINSEQ_1:1;
then
i in dom PR
by FINSEQ_1:def 3;
then A15:
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
j <= len PR
by A12, A14, XXREAL_0:2;
then
j in dom PR
by A11, FINSEQ_3:25;
then
PR . j = (PR ^ PR1) . j
by FINSEQ_1:def 7;
hence
ex
i,
j being
Nat ex
f,
g being
FinSequence of
CQC-WFF Al st
( 1
<= i &
i < n & 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) `1 )
by A3, A9, A10, A11, A12, A13, A15;
verum end; case
((PR ^ PR1) . n) `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 & 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) `1 )then consider i,
j being
Nat,
f,
g being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al such that A16:
1
<= i
and A17:
i < n
and A18:
1
<= j
and A19:
j < i
and A20:
(
len f > 1 &
Ant f = Ant g &
Suc (Ant f) = 'not' p &
'not' (Suc f) = Suc g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*p*> = (PR . n) `1 )
by A3, A5, Def7;
A21:
i <= len PR
by A2, A17, XXREAL_0:2;
then
i in Seg (len PR)
by A16, FINSEQ_1:1;
then
i in dom PR
by FINSEQ_1:def 3;
then A22:
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
j <= len PR
by A19, A21, XXREAL_0:2;
then
j in dom PR
by A18, FINSEQ_3:25;
then
PR . j = (PR ^ PR1) . j
by FINSEQ_1:def 7;
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 & 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) `1 )
by A3, A16, A17, A18, A19, A20, A22;
verum end; case
((PR ^ PR1) . n) `2 = 5
;
ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n & 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) `1 )then consider i,
j being
Nat,
f,
g being
FinSequence of
CQC-WFF Al such that A23:
1
<= i
and A24:
i < n
and A25:
1
<= j
and A26:
j < i
and A27:
(
Ant f = Ant g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 )
by A3, A5, Def7;
A28:
i <= len PR
by A2, A24, XXREAL_0:2;
then
i in Seg (len PR)
by A23, FINSEQ_1:1;
then
i in dom PR
by FINSEQ_1:def 3;
then A29:
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
j <= len PR
by A26, A28, XXREAL_0:2;
then
j in dom PR
by A25, FINSEQ_3:25;
then
PR . j = (PR ^ PR1) . j
by FINSEQ_1:def 7;
hence
ex
i,
j being
Nat ex
f,
g being
FinSequence of
CQC-WFF Al st
( 1
<= i &
i < n & 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) `1 )
by A3, A23, A24, A25, A26, A27, A29;
verum end; case
((PR ^ PR1) . n) `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 & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 )then consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A30:
1
<= i
and A31:
i < n
and A32:
(
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*p*> = (PR . n) `1 )
by A3, A5, Def7;
i <= len PR
by A2, A31, XXREAL_0:2;
then
i in dom PR
by A30, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
p '&' q = Suc f &
f = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 )
by A3, A30, A31, A32;
verum end; case
((PR ^ PR1) . n) `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 & p '&' q = Suc f & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 )then consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A33:
1
<= i
and A34:
i < n
and A35:
(
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*q*> = (PR . n) `1 )
by A3, A5, Def7;
i <= len PR
by A2, A34, XXREAL_0:2;
then
i in dom PR
by A33, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
p '&' q = Suc f &
f = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 )
by A3, A33, A34, A35;
verum end; case
((PR ^ PR1) . n) `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 & Suc f = All (x,p) & f = ((PR ^ PR1) . i) `1 & (Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `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 A36:
1
<= i
and A37:
i < n
and A38:
(
Suc f = All (
x,
p) &
f = (PR . i) `1 &
(Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 )
by A3, A5, Def7;
i <= len PR
by A2, A37, XXREAL_0:2;
then
i in dom PR
by A36, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
Suc f = All (
x,
p) &
f = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 )
by A3, A36, A37, A38;
verum end; case
((PR ^ PR1) . n) `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 & 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) `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 A39:
1
<= i
and A40:
i < n
and A41:
(
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 . i) `1 &
(Ant f) ^ <*(All (x,p))*> = (PR . n) `1 )
by A3, A5, Def7;
i <= len PR
by A2, A40, XXREAL_0:2;
then
i in dom PR
by A39, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
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) `1 )
by A3, A39, A40, A41;
verum end; end;
end;
assume A42:
PR ^ PR1,n is_a_correct_step
; PR,n is_a_correct_step
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9
by A1, A2, Th31;
per cases then
( (PR . n) `2 = 0 or (PR . n) `2 = 1 or (PR . n) `2 = 2 or (PR . n) `2 = 3 or (PR . n) `2 = 4 or (PR . n) `2 = 5 or (PR . n) `2 = 6 or (PR . n) `2 = 7 or (PR . n) `2 = 8 or (PR . n) `2 = 9 )
;
CALCUL_1:def 7case
(PR . n) `2 = 2
;
ex i being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g )then consider i being
Nat,
f,
g being
FinSequence of
CQC-WFF Al such that A43:
1
<= i
and A44:
i < n
and A45:
(
Ant f is_Subsequence_of Ant g &
Suc f = Suc g &
((PR ^ PR1) . i) `1 = f &
((PR ^ PR1) . n) `1 = g )
by A3, A42, Def7;
i <= len PR
by A2, A44, XXREAL_0:2;
then
i in dom PR
by A43, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
hence
ex
i being
Nat ex
f,
g being
FinSequence of
CQC-WFF Al st
( 1
<= i &
i < n &
Ant f is_Subsequence_of Ant g &
Suc f = Suc g &
(PR . i) `1 = f &
(PR . n) `1 = g )
by A3, A43, A44, A45;
verum end; case
(PR . n) `2 = 3
;
ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n & 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 . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 )then consider i,
j being
Nat,
f,
f1 being
FinSequence of
CQC-WFF Al such that A46:
1
<= i
and A47:
i < n
and A48:
1
<= j
and A49:
j < i
and A50:
(
len f > 1 &
len f1 > 1 &
Ant (Ant f) = Ant (Ant f1) &
'not' (Suc (Ant f)) = Suc (Ant f1) &
Suc f = Suc f1 &
f = ((PR ^ PR1) . j) `1 &
f1 = ((PR ^ PR1) . i) `1 &
(Ant (Ant f)) ^ <*(Suc f)*> = ((PR ^ PR1) . n) `1 )
by A3, A42, Def7;
A51:
i <= len PR
by A2, A47, XXREAL_0:2;
then
i in Seg (len PR)
by A46, FINSEQ_1:1;
then
i in dom PR
by FINSEQ_1:def 3;
then A52:
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
j <= len PR
by A49, A51, XXREAL_0:2;
then
j in dom PR
by A48, FINSEQ_3:25;
then
PR . j = (PR ^ PR1) . j
by FINSEQ_1:def 7;
hence
ex
i,
j being
Nat ex
f,
g being
FinSequence of
CQC-WFF Al st
( 1
<= i &
i < n & 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 . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 )
by A3, A46, A47, A48, A49, A50, A52;
verum end; case
(PR . n) `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 & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 )then consider i,
j being
Nat,
f,
g being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al such that A53:
1
<= i
and A54:
i < n
and A55:
1
<= j
and A56:
j < i
and A57:
(
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) `1 )
by A3, A42, Def7;
A58:
i <= len PR
by A2, A54, XXREAL_0:2;
then
i in Seg (len PR)
by A53, FINSEQ_1:1;
then
i in dom PR
by FINSEQ_1:def 3;
then A59:
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
j <= len PR
by A56, A58, XXREAL_0:2;
then
j in dom PR
by A55, FINSEQ_3:25;
then
PR . j = (PR ^ PR1) . j
by FINSEQ_1:def 7;
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 & 1
<= j &
j < i &
len f > 1 &
Ant f = Ant g &
Suc (Ant f) = 'not' p &
'not' (Suc f) = Suc g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant (Ant f)) ^ <*p*> = (PR . n) `1 )
by A3, A53, A54, A55, A56, A57, A59;
verum end; case
(PR . n) `2 = 5
;
ex i, j being Nat ex f, g being FinSequence of CQC-WFF Al st
( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 )then consider i,
j being
Nat,
f,
g being
FinSequence of
CQC-WFF Al such that A60:
1
<= i
and A61:
i < n
and A62:
1
<= j
and A63:
j < i
and A64:
(
Ant f = Ant g &
f = ((PR ^ PR1) . j) `1 &
g = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*((Suc f) '&' (Suc g))*> = ((PR ^ PR1) . n) `1 )
by A3, A42, Def7;
A65:
i <= len PR
by A2, A61, XXREAL_0:2;
then
i in Seg (len PR)
by A60, FINSEQ_1:1;
then
i in dom PR
by FINSEQ_1:def 3;
then A66:
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
j <= len PR
by A63, A65, XXREAL_0:2;
then
j in dom PR
by A62, FINSEQ_3:25;
then
PR . j = (PR ^ PR1) . j
by FINSEQ_1:def 7;
hence
ex
i,
j being
Nat ex
f,
g being
FinSequence of
CQC-WFF Al st
( 1
<= i &
i < n & 1
<= j &
j < i &
Ant f = Ant g &
f = (PR . j) `1 &
g = (PR . i) `1 &
(Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 )
by A3, A60, A61, A62, A63, A64, A66;
verum end; case
(PR . n) `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 & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 )then consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A67:
1
<= i
and A68:
i < n
and A69:
(
p '&' q = Suc f &
f = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*p*> = ((PR ^ PR1) . n) `1 )
by A3, A42, Def7;
i <= len PR
by A2, A68, XXREAL_0:2;
then
i in dom PR
by A67, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*p*> = (PR . n) `1 )
by A3, A67, A68, A69;
verum end; case
(PR . n) `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 & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 )then consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A70:
1
<= i
and A71:
i < n
and A72:
(
p '&' q = Suc f &
f = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*q*> = ((PR ^ PR1) . n) `1 )
by A3, A42, Def7;
i <= len PR
by A2, A71, XXREAL_0:2;
then
i in dom PR
by A70, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*q*> = (PR . n) `1 )
by A3, A70, A71, A72;
verum end; case
(PR . n) `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 & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `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 A73:
1
<= i
and A74:
i < n
and A75:
(
Suc f = All (
x,
p) &
f = ((PR ^ PR1) . i) `1 &
(Ant f) ^ <*(p . (x,y))*> = ((PR ^ PR1) . n) `1 )
by A3, A42, Def7;
i <= len PR
by A2, A74, XXREAL_0:2;
then
i in dom PR
by A73, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
Suc f = All (
x,
p) &
f = (PR . i) `1 &
(Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 )
by A3, A73, A74, A75;
verum end; case
(PR . n) `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 & 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 . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `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 A76:
1
<= i
and A77:
i < n
and A78:
(
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) `1 )
by A3, A42, Def7;
i <= len PR
by A2, A77, XXREAL_0:2;
then
i in dom PR
by A76, FINSEQ_3:25;
then
PR . i = (PR ^ PR1) . i
by FINSEQ_1:def 7;
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 &
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 . i) `1 &
(Ant f) ^ <*(All (x,p))*> = (PR . n) `1 )
by A3, A76, A77, A78;
verum end; end;