let Al be QC-alphabet ; for f, g being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds
|- f ^ <*(Impl (Rev g))*>
let f, g be FinSequence of CQC-WFF Al; ( 1 <= len g & |- f ^ g implies |- f ^ <*(Impl (Rev g))*> )
set h = Rev g;
assume that
A1:
1 <= len g
and
A2:
|- f ^ g
; |- f ^ <*(Impl (Rev g))*>
A3:
1 <= len (Rev g)
by A1, FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF Al such that
A4:
Impl (Rev g) = F . (len (Rev g))
and
A5:
len F = len (Rev g)
and
A6:
( F . 1 = Begin (Rev g) or len (Rev g) = 0 )
and
A7:
for n being Nat st 1 <= n & n < len (Rev g) holds
ex p, q being Element of CQC-WFF Al st
( p = (Rev g) . (n + 1) & q = F . n & F . (n + 1) = p => q )
by Def4;
A8:
1 <= len (Rev g)
by A1, FINSEQ_5:def 3;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len F implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( $1 + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . $1)*> & |- f2 ) );
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]
A11:
len g <= len (f ^ g)
by CALCUL_1:6;
assume that A12:
1
<= k + 1
and A13:
k + 1
<= len F
;
ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )
A14:
k + 1
<= len g
by A5, A13, FINSEQ_5:def 3;
then consider n being
Nat such that A15:
len (f ^ g) = (k + 1) + n
by A11, NAT_1:10, XXREAL_0:2;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
A16:
now ( k <> 0 implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) )
k + 1
in dom F
by A12, A13, FINSEQ_3:25;
then reconsider r =
F . (k + 1) as
Element of
CQC-WFF Al by FINSEQ_2:11;
set f1 =
(f ^ g) | (Seg n);
reconsider f1 =
(f ^ g) | (Seg n) as
FinSequence of
CQC-WFF Al by FINSEQ_1:18;
set f2 =
f1 ^ <*r*>;
len (f ^ g) <= (len (f ^ g)) + k
by NAT_1:11;
then A17:
(len (f ^ g)) - k <= ((len (f ^ g)) + k) - k
by XREAL_1:9;
assume
k <> 0
;
ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )then A18:
0 + 1
<= k
by NAT_1:13;
then consider f1k being
FinSequence of
CQC-WFF Al such that A19:
ex
f2 being
FinSequence of
CQC-WFF Al ex
n being
Element of
NAT st
(
k + n = len (f ^ g) &
f1k = (f ^ g) | (Seg n) &
f2 = f1k ^ <*(F . k)*> &
|- f2 )
by A10, A13, NAT_1:13;
consider f2k being
FinSequence of
CQC-WFF Al such that A20:
ex
n being
Element of
NAT st
(
k + n = len (f ^ g) &
f1k = (f ^ g) | (Seg n) &
f2k = f1k ^ <*(F . k)*> &
|- f2k )
by A19;
consider nk being
Element of
NAT such that A21:
k + nk = len (f ^ g)
and A22:
(
f1k = (f ^ g) | (Seg nk) &
f2k = f1k ^ <*(F . k)*> )
and A23:
|- f2k
by A20;
1
<= n + 1
by NAT_1:11;
then A24:
nk in dom (f ^ g)
by A15, A21, A17, FINSEQ_3:25;
then reconsider p =
(f ^ g) . nk as
Element of
CQC-WFF Al by FINSEQ_2:11;
n + 1
= nk
by A15, A21;
then A25:
f2k = (f1 ^ <*((f ^ g) . nk)*>) ^ <*(F . k)*>
by A22, A24, FINSEQ_5:10;
A26:
k < len (Rev g)
by A5, A13, NAT_1:13;
then consider p1,
q1 being
Element of
CQC-WFF Al such that A27:
p1 = (Rev g) . (k + 1)
and A28:
(
q1 = F . k &
F . (k + 1) = p1 => q1 )
by A7, A18;
k + 1
in dom (Rev g)
by A5, A12, A13, FINSEQ_3:25;
then
k + 1
in dom g
by FINSEQ_5:57;
then A29:
p1 =
g . (((len g) - (k + 1)) + 1)
by A27, FINSEQ_5:58
.=
g . ((len g) - k)
;
k < len g
by A26, FINSEQ_5:def 3;
then A30:
k + (- k) < (len g) + (- k)
by XREAL_1:8;
then reconsider i =
(len g) - k as
Element of
NAT by INT_1:3;
len g <= k + (len g)
by NAT_1:11;
then A31:
i <= len g
by XREAL_1:20;
0 + 1
<= i
by A30, INT_1:7;
then
i in dom g
by A31, FINSEQ_3:25;
then p1 =
(f ^ g) . ((len f) + i)
by A29, FINSEQ_1:def 7
.=
(f ^ g) . (((len f) + (len g)) - k)
.=
(f ^ g) . ((len (f ^ g)) - k)
by FINSEQ_1:22
.=
p
by A21
;
then
|- f1 ^ <*r*>
by A23, A25, A28, Th27;
hence
ex
f1,
f2 being
FinSequence of
CQC-WFF Al ex
n being
Element of
NAT st
(
(k + 1) + n = len (f ^ g) &
f1 = (f ^ g) | (Seg n) &
f2 = f1 ^ <*(F . (k + 1))*> &
|- f2 )
by A15;
verum end;
A32:
k + 1
<= len (f ^ g)
by A14, A11, XXREAL_0:2;
now ( k = 0 implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) )
F . 1
= (Rev g) . 1
by A3, A6, Def3;
then A33:
F . 1
= g . (len g)
by FINSEQ_5:62;
set f1 =
(f ^ g) | (Seg n);
reconsider f1 =
(f ^ g) | (Seg n) as
FinSequence of
CQC-WFF Al by FINSEQ_1:18;
set f2 =
f1 ^ <*(F . 1)*>;
A34:
len g in dom g
by A1, FINSEQ_3:25;
assume A35:
k = 0
;
ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )then A36:
(f ^ g) . (n + 1) = (f ^ g) . ((len f) + (len g))
by A15, FINSEQ_1:22;
1
<= len (f ^ g)
by A12, A32, XXREAL_0:2;
then
len (f ^ g) in dom (f ^ g)
by FINSEQ_3:25;
then
(f ^ g) | (Seg (n + 1)) = f1 ^ <*((f ^ g) . (n + 1))*>
by A15, A35, FINSEQ_5:10;
then
f1 ^ <*(F . 1)*> = (f ^ g) | (Seg (len (f ^ g)))
by A15, A35, A33, A34, A36, FINSEQ_1:def 7;
then A37:
f1 ^ <*(F . 1)*> = (f ^ g) | (dom (f ^ g))
by FINSEQ_1:def 3;
then reconsider f2 =
f1 ^ <*(F . 1)*> as
FinSequence of
CQC-WFF Al by RELAT_1:69;
take f1 =
f1;
ex f2 being FinSequence of CQC-WFF Al ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )take f2 =
f2;
ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )take n =
n;
ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )
|- f2
by A2, A37, RELAT_1:69;
hence
ex
f1,
f2 being
FinSequence of
CQC-WFF Al ex
n being
Element of
NAT st
(
(k + 1) + n = len (f ^ g) &
f1 = (f ^ g) | (Seg n) &
f2 = f1 ^ <*(F . (k + 1))*> &
|- f2 )
by A15, A35;
verum end;
hence
ex
f1,
f2 being
FinSequence of
CQC-WFF Al ex
n being
Element of
NAT st
(
(k + 1) + n = len (f ^ g) &
f1 = (f ^ g) | (Seg n) &
f2 = f1 ^ <*(F . (k + 1))*> &
|- f2 )
by A16;
verum
end;
A38:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A38, A9);
then consider f1 being FinSequence of CQC-WFF Al such that
A39:
ex f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (len (Rev g)) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (len (Rev g)))*> & |- f2 )
by A5, A8;
consider f2 being FinSequence of CQC-WFF Al such that
A40:
ex n being Element of NAT st
( (len (Rev g)) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (len (Rev g)))*> & |- f2 )
by A39;
consider n being Element of NAT such that
A41:
(len (Rev g)) + n = len (f ^ g)
and
A42:
( f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (len (Rev g)))*> & |- f2 )
by A40;
(n + (len (Rev g))) - (len (Rev g)) = (len (f ^ g)) - (len g)
by A41, FINSEQ_5:def 3;
then
(n + (len (Rev g))) + (- (len (Rev g))) = ((len f) + (len g)) - (len g)
by FINSEQ_1:22;
then
Seg n = dom f
by FINSEQ_1:def 3;
hence
|- f ^ <*(Impl (Rev g))*>
by A4, A42, FINSEQ_1:21; verum