let Al be QC-alphabet ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( |- (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 S_{1}[ 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*>)))*> ; :: thesis: |- (Per (f,P)) ^ <*p*>

A9: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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); :: thesis: ( |- (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 S

( p = (Rev F) . $1 & |- (Per (f,P)) ^ <*p*> ) );

assume A8: |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> ; :: thesis: |- (Per (f,P)) ^ <*p*>

A9: for k being Nat st S

S

proof

A37:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A10: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume that

A11: 1 <= k + 1 and

A12: k + 1 <= len (Rev F) ; :: thesis: ex p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A13; :: thesis: verum

end;assume A10: S

assume that

A11: 1 <= k + 1 and

A12: k + 1 <= len (Rev F) ; :: thesis: ex p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

A13: now :: thesis: ( k <> 0 implies ex q1, p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) )

( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

now :: thesis: ( k = 0 implies ex p, p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) )

hence
ex p being Element of CQC-WFF Al st ( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) )

1 <= len (Rev F)
by A2, A4, FINSEQ_5:def 3;

then A35: 1 in dom (Rev F) by FINSEQ_3:25;

then reconsider p = (Rev F) . 1 as Element of CQC-WFF Al by FINSEQ_2:11;

assume A36: k = 0 ; :: thesis: ex p, p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

take p = p; :: thesis: ex p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

1 in dom F by A35, FINSEQ_5:57;

then p = F . (((len F) - 1) + 1) by FINSEQ_5:58

.= Impl (Rev (f ^ <*p*>)) by A3, A4 ;

hence ex p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A8, A36; :: thesis: verum

end;then A35: 1 in dom (Rev F) by FINSEQ_3:25;

then reconsider p = (Rev F) . 1 as Element of CQC-WFF Al by FINSEQ_2:11;

assume A36: k = 0 ; :: thesis: ex p, p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

take p = p; :: thesis: ex p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> )

1 in dom F by A35, FINSEQ_5:57;

then p = F . (((len F) - 1) + 1) by FINSEQ_5:58

.= Impl (Rev (f ^ <*p*>)) by A3, A4 ;

hence ex p being Element of CQC-WFF Al st

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A8, A36; :: thesis: verum

( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A13; :: thesis: verum

for k being Nat holds S

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; :: thesis: verum