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