let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al
for n being Nat st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
let p, q be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al
for n being Nat st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
let f be FinSequence of CQC-WFF Al; :: thesis: for n being Nat st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
let n be Nat; :: thesis: ( 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> implies |- (f ^ <*p*>) ^ <*q*> )
assume that
A1: 1 <= n and
A2: |- (f ^ (IdFinS (p,n))) ^ <*q*> ; :: thesis: |- (f ^ <*p*>) ^ <*q*>
set g = (f ^ (IdFinS (p,n))) ^ <*q*>;
set h = Rev ((f ^ (IdFinS (p,n))) ^ <*q*>);
A3: 1 <= len ((f ^ (IdFinS (p,n))) ^ <*q*>) by CALCUL_1:10;
then A4: 1 <= len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF Al such that
A5: Impl (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) = F . (len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>))) and
A6: len F = len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) and
A7: ( F . 1 = Begin (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) or len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) = 0 ) and
A8: for n being Nat st 1 <= n & n < len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) holds
ex p, q being Element of CQC-WFF Al st
( p = (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) . (n + 1) & q = F . n & F . (n + 1) = p => q ) by Def4;
set H = Rev F;
A9: 1 <= len (Rev F) by A4, A6, FINSEQ_5:def 3;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len (Rev F) implies ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . $1 & |- (f ^ <*p*>) ^ <*p1*> ) );
|- ((f ^ <*p*>) ^ (f ^ (IdFinS (p,n)))) ^ <*q*> by A2, Th20;
then |- (f ^ <*p*>) ^ ((f ^ (IdFinS (p,n))) ^ <*q*>) by FINSEQ_1:32;
then A10: |- (f ^ <*p*>) ^ <*(Impl (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)))*> by A3, Th28;
A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
assume that
A13: 1 <= k + 1 and
A14: k + 1 <= len (Rev F) ; :: thesis: ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )

A15: now :: thesis: ( k <> 0 implies ex q1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) )

A16: k < len (Rev F) by A14, NAT_1:13;
then 0 + k < len F by FINSEQ_5:def 3;
then A17: (0 + k) + (- k) < (len F) + (- k) by XREAL_1:8;
then reconsider i = (len F) - k as Element of NAT by INT_1:3;
A18: (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - i = (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - ((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - k) by A6, FINSEQ_5:def 3
.= k ;
A19: 0 + 1 <= i by A17, NAT_1:13;
then A20: 1 <= i + 1 by NAT_1:13;
assume A21: k <> 0 ; :: thesis: ex q1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
then A22: 0 + 1 <= k by NAT_1:13;
then consider pk being Element of CQC-WFF Al such that
A23: pk = (Rev F) . k and
A24: |- (f ^ <*p*>) ^ <*pk*> by A12, A14, NAT_1:13;
len F < (len F) + k by A21, XREAL_1:29;
then A25: (len F) + (- k) < ((len F) + k) + (- k) by XREAL_1:8;
then consider p1, q1 being Element of CQC-WFF Al such that
A26: p1 = (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) . (i + 1) and
A27: q1 = F . i and
A28: F . (i + 1) = p1 => q1 by A6, A8, A19;
set g1 = (f ^ <*p*>) ^ <*p1*>;
A29: Suc ((f ^ <*p*>) ^ <*p1*>) = p1 by CALCUL_1:5;
len ((f ^ (IdFinS (p,n))) ^ <*q*>) < (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) + i by A17, XREAL_1:29;
then (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) + (- i) < ((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) + i) + (- i) by XREAL_1:8;
then k < (len (f ^ (IdFinS (p,n)))) + (len <*q*>) by FINSEQ_1:22, A18;
then k < (len (f ^ (IdFinS (p,n)))) + 1 by FINSEQ_1:39;
then k <= len (f ^ (IdFinS (p,n))) by NAT_1:13;
then A30: k in dom (f ^ (IdFinS (p,n))) by A22, FINSEQ_3:25;
then A31: ((f ^ (IdFinS (p,n))) ^ <*q*>) . k = (((f ^ (IdFinS (p,n))) ^ <*q*>) | (dom (f ^ (IdFinS (p,n))))) . k by FUNCT_1:49;
A32: (f ^ (IdFinS (p,n))) . k in rng (f ^ (IdFinS (p,n))) by A30, FUNCT_1:3;
rng (f ^ (IdFinS (p,n))) = (rng f) \/ (rng (IdFinS (p,n))) by FINSEQ_1:31
.= (rng f) \/ (rng <*p*>) by A1, Th31
.= rng (f ^ <*p*>) by FINSEQ_1:31 ;
then A33: (f ^ (IdFinS (p,n))) . k in rng (Ant ((f ^ <*p*>) ^ <*p1*>)) by A32, CALCUL_1:5;
i + 1 <= len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A6, A25, NAT_1:13;
then i + 1 in dom (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A20, FINSEQ_3:25;
then i + 1 in dom ((f ^ (IdFinS (p,n))) ^ <*q*>) by FINSEQ_5:57;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . (((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - (i + 1)) + 1) by A26, FINSEQ_5:58
.= ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - i) ;
then p1 = (f ^ (IdFinS (p,n))) . k by A31, FINSEQ_1:21, A18;
then ex j1 being Nat st
( j1 in dom (Ant ((f ^ <*p*>) ^ <*p1*>)) & (Ant ((f ^ <*p*>) ^ <*p1*>)) . j1 = p1 ) by A33, FINSEQ_2:10;
then Suc ((f ^ <*p*>) ^ <*p1*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p1*>) by A29, CALCUL_1:def 16;
then A34: |- (f ^ <*p*>) ^ <*p1*> by CALCUL_1:33;
take q1 = q1; :: thesis: ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
k + 1 in dom (Rev F) by A13, A14, FINSEQ_3:25;
then ( i = ((len F) - (k + 1)) + 1 & k + 1 in dom F ) by FINSEQ_5:57;
then A35: q1 = (Rev F) . (k + 1) by A27, FINSEQ_5:58;
k in dom (Rev F) by A22, A16, FINSEQ_3:25;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by A23, A28, FINSEQ_5:58;
then |- (f ^ <*p*>) ^ <*q1*> by A24, A34, CALCUL_1:56;
hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A35; :: thesis: verum

end;

now :: thesis: ( k = 0 implies ex p1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) )

len (Rev F) = len (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A6, FINSEQ_5:def 3;
then A36: 1 in dom (Rev F) by A4, FINSEQ_3:25;
then reconsider p1 = (Rev F) . 1 as Element of CQC-WFF Al by FINSEQ_2:11;
assume A37: k = 0 ; :: thesis: ex p1, p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
take p1 = p1; :: thesis: ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> )
1 in dom F by A36, FINSEQ_5:57;
then p1 = F . (((len F) - 1) + 1) by FINSEQ_5:58
.= Impl (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A5, A6 ;
hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A10, A37; :: thesis: verum

end;

hence ex p1 being Element of CQC-WFF Al st
( p1 = (Rev F) . (k + 1) & |- (f ^ <*p*>) ^ <*p1*> ) by A15; :: thesis: verum

end;

A38: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A38, A11);
then consider p1 being Element of CQC-WFF Al such that
A39: p1 = (Rev F) . (len (Rev F)) and
A40: |- (f ^ <*p*>) ^ <*p1*> by A9;
p1 = (Rev F) . (len F) by A39, FINSEQ_5:def 3;
then p1 = Begin (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) by A3, A7, FINSEQ_5:62, FINSEQ_5:def 3;
then p1 = (Rev ((f ^ (IdFinS (p,n))) ^ <*q*>)) . 1 by A4, Def3;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) by FINSEQ_5:62;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len (f ^ (IdFinS (p,n)))) + (len <*q*>)) by FINSEQ_1:22;
then p1 = ((f ^ (IdFinS (p,n))) ^ <*q*>) . ((len (f ^ (IdFinS (p,n)))) + 1) by FINSEQ_1:39;
hence |- (f ^ <*p*>) ^ <*q*> by A40, FINSEQ_1:42; :: thesis: verum