let Al be QC-alphabet ; for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) st |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds
|- (Per (f,P)) ^ <*p*>
let p be Element of CQC-WFF Al; for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) st |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds
|- (Per (f,P)) ^ <*p*>
let f be FinSequence of CQC-WFF Al; for P being Permutation of (dom f) st |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds
|- (Per (f,P)) ^ <*p*>
let P be Permutation of (dom f); ( |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> implies |- (Per (f,P)) ^ <*p*> )
set g = f ^ <*p*>;
set h = Rev (f ^ <*p*>);
A1:
1 <= len (f ^ <*p*>)
by CALCUL_1:10;
then A2:
1 <= len (Rev (f ^ <*p*>))
by FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF Al such that
A3:
Impl (Rev (f ^ <*p*>)) = F . (len (Rev (f ^ <*p*>)))
and
A4:
len F = len (Rev (f ^ <*p*>))
and
A5:
( F . 1 = Begin (Rev (f ^ <*p*>)) or len (Rev (f ^ <*p*>)) = 0 )
and
A6:
for n being Nat st 1 <= n & n < len (Rev (f ^ <*p*>)) holds
ex p, q being Element of CQC-WFF Al st
( p = (Rev (f ^ <*p*>)) . (n + 1) & q = F . n & F . (n + 1) = p => q )
by Def4;
set H = Rev F;
A7:
1 <= len (Rev F)
by A2, A4, FINSEQ_5:def 3;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len (Rev F) implies ex p being Element of CQC-WFF Al st
( p = (Rev F) . $1 & |- (Per (f,P)) ^ <*p*> ) );
assume A8:
|- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*>
; |- (Per (f,P)) ^ <*p*>
A9:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A10:
S1[
k]
;
S1[k + 1]
assume that A11:
1
<= k + 1
and A12:
k + 1
<= len (Rev F)
;
ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )
A13:
now ( k <> 0 implies ex q1, p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) )A14:
k < len (Rev F)
by A12, NAT_1:13;
then
0 + k < len F
by FINSEQ_5:def 3;
then A15:
(0 + k) + (- k) < (len F) + (- k)
by XREAL_1:8;
then reconsider i =
(len F) - k as
Element of
NAT by INT_1:3;
A16:
(len (f ^ <*p*>)) - i =
(len (f ^ <*p*>)) - ((len (f ^ <*p*>)) - k)
by A4, FINSEQ_5:def 3
.=
k
;
then reconsider j =
(len (f ^ <*p*>)) - i as
Nat ;
A17:
0 + 1
<= i
by A15, NAT_1:13;
then A18:
1
<= i + 1
by NAT_1:13;
assume A19:
k <> 0
;
ex q1, p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )then A20:
0 + 1
<= k
by NAT_1:13;
then consider pk being
Element of
CQC-WFF Al such that A21:
pk = (Rev F) . k
and A22:
|- (Per (f,P)) ^ <*pk*>
by A10, A12, NAT_1:13;
len F < (len F) + k
by A19, XREAL_1:29;
then A23:
(len F) + (- k) < ((len F) + k) + (- k)
by XREAL_1:8;
then consider p1,
q1 being
Element of
CQC-WFF Al such that A24:
p1 = (Rev (f ^ <*p*>)) . (i + 1)
and A25:
q1 = F . i
and A26:
F . (i + 1) = p1 => q1
by A4, A6, A17;
take q1 =
q1;
ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )
k + 1
in dom (Rev F)
by A11, A12, FINSEQ_3:25;
then
(
i = ((len F) - (k + 1)) + 1 &
k + 1
in dom F )
by FINSEQ_5:57;
then A27:
q1 = (Rev F) . (k + 1)
by A25, FINSEQ_5:58;
len (f ^ <*p*>) < (len (f ^ <*p*>)) + i
by A15, XREAL_1:29;
then
(len (f ^ <*p*>)) + (- i) < ((len (f ^ <*p*>)) + i) + (- i)
by XREAL_1:8;
then
j < (len f) + (len <*p*>)
by FINSEQ_1:22;
then
j < (len f) + 1
by FINSEQ_1:39;
then
j <= len f
by NAT_1:13;
then A28:
j in dom f
by A20, A16, FINSEQ_3:25;
then A29:
(f ^ <*p*>) . j = ((f ^ <*p*>) | (dom f)) . j
by FUNCT_1:49;
j in rng P
by A28, FUNCT_2:def 3;
then consider a being
object such that A30:
a in dom P
and A31:
P . a = j
by FUNCT_1:def 3;
A32:
a in dom f
by A30;
then reconsider j1 =
a as
Element of
NAT ;
set g1 =
(Per (f,P)) ^ <*p1*>;
i + 1
<= len (Rev (f ^ <*p*>))
by A4, A23, NAT_1:13;
then
i + 1
in dom (Rev (f ^ <*p*>))
by A18, FINSEQ_3:25;
then
i + 1
in dom (f ^ <*p*>)
by FINSEQ_5:57;
then p1 =
(f ^ <*p*>) . (((len (f ^ <*p*>)) - (i + 1)) + 1)
by A24, FINSEQ_5:58
.=
(f ^ <*p*>) . ((len (f ^ <*p*>)) - i)
;
then
p1 = f . (P . j1)
by A29, A31, FINSEQ_1:21;
then
p1 = (P * f) . j1
by A30, FUNCT_1:13;
then
Suc ((Per (f,P)) ^ <*p1*>) = (Per (f,P)) . j1
by CALCUL_1:5;
then A33:
Suc ((Per (f,P)) ^ <*p1*>) = (Ant ((Per (f,P)) ^ <*p1*>)) . j1
by CALCUL_1:5;
j1 in dom (Per (f,P))
by A32, Th19;
then
j1 in dom (Ant ((Per (f,P)) ^ <*p1*>))
by CALCUL_1:5;
then
Suc ((Per (f,P)) ^ <*p1*>) is_tail_of Ant ((Per (f,P)) ^ <*p1*>)
by A33, CALCUL_1:def 16;
then A34:
|- (Per (f,P)) ^ <*p1*>
by CALCUL_1:33;
k in dom (Rev F)
by A20, A14, FINSEQ_3:25;
then
k in dom F
by FINSEQ_5:57;
then
pk = p1 => q1
by A21, A26, FINSEQ_5:58;
then
|- (Per (f,P)) ^ <*q1*>
by A22, A34, CALCUL_1:56;
hence
ex
p being
Element of
CQC-WFF Al st
(
p = (Rev F) . (k + 1) &
|- (Per (f,P)) ^ <*p*> )
by A27;
verum end;
hence
ex
p being
Element of
CQC-WFF Al st
(
p = (Rev F) . (k + 1) &
|- (Per (f,P)) ^ <*p*> )
by A13;
verum
end;
A37:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A37, A9);
then consider q being Element of CQC-WFF Al such that
A38:
q = (Rev F) . (len (Rev F))
and
A39:
|- (Per (f,P)) ^ <*q*>
by A7;
q = (Rev F) . (len F)
by A38, FINSEQ_5:def 3;
then
q = Begin (Rev (f ^ <*p*>))
by A1, A5, FINSEQ_5:62, FINSEQ_5:def 3;
then
q = (Rev (f ^ <*p*>)) . 1
by A2, Def3;
then
q = (f ^ <*p*>) . (len (f ^ <*p*>))
by FINSEQ_5:62;
then
q = (f ^ <*p*>) . ((len f) + (len <*p*>))
by FINSEQ_1:22;
then
q = (f ^ <*p*>) . ((len f) + 1)
by FINSEQ_1:39;
hence
|- (Per (f,P)) ^ <*p*>
by A39, FINSEQ_1:42; verum