:: CALCUL_2 semantic presentation

begin


definition
let m, n be natural number ;
func seq (m,n) ->  set  equals :: CALCUL_2:def 1
 {  k where k is Element of NAT : ( 1 + m <= k & k <= n + m )  }  ;
coherence
  {  k where k is Element of NAT : ( 1 + m <= k & k <= n + m )  }  is set ;
end;

:: deftheorem  defines seq CALCUL_2:def_1_:_
 for m, n being natural number holds seq (m,n) =  {  k where k is Element of NAT : ( 1 + m <= k & k <= n + m )  }  ;

definition
let m, n be natural number ;
:: original: seq
redefine func seq (m,n) ->  Subset of NAT;
coherence
 seq (m,n) is Subset of NAT
proof
set X = seq (m,n);
 seq (m,n) c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in seq (m,n) or x in NAT )
assume  x in seq (m,n) ; ::_thesis: x in NAT
then  ex i being Element of NAT st
( x = i & 1 + m <= i & i <= n + m ) ;
hence  x in NAT ; ::_thesis: verum
end;
hence  seq (m,n) is Subset of NAT ; ::_thesis: verum
end;
end;

theorem Th1: :: CALCUL_2:1
for c, a, b being natural number holds
( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) )
proof
let c, a, b be natural number ; ::_thesis: ( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) )
A1: ( c in  {  m where m is Element of NAT : ( 1 + a <= m & m <= b + a )  }  iff ex m being Element of NAT st
( c = m & 1 + a <= m & m <= b + a ) ) ;
 c is Element of NAT by ORDINAL1:def_12;
hence  ( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) ) by A1; ::_thesis: verum
end;

theorem Th2: :: CALCUL_2:2
for a being natural number holds seq (a,0) = {}
proof
let a be natural number ; ::_thesis: seq (a,0) = {}
hereby  ::_thesis: verum
set x = the Element of seq (a,0);
assume A1: seq (a,0) <> {} ; ::_thesis: contradiction
then reconsider x = the Element of seq (a,0) as Element of NAT by TARSKI:def_3;
 ( 1 + a <= x & x <= 0 + a ) by A1, Th1;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
end;

theorem Th3: :: CALCUL_2:3
for b, a being natural number holds
( b = 0 or b + a in seq (a,b) )
proof
let b, a be natural number ; ::_thesis: ( b = 0 or b + a in seq (a,b) )
assume  b <> 0 ; ::_thesis: b + a in seq (a,b)
then  ex c being Nat st b = c + 1 by NAT_1:6;
then  1 <= b by NAT_1:11;
then  ( b + a is Element of NAT & 1 + a <= b + a ) by ORDINAL1:def_12, XREAL_1:6;
hence  b + a in seq (a,b) ; ::_thesis: verum
end;

theorem Th4: :: CALCUL_2:4
for b1, b2, a being natural number holds
( b1 <= b2 iff seq (a,b1) c= seq (a,b2) )
proof
let b1, b2, a be natural number ; ::_thesis: ( b1 <= b2 iff seq (a,b1) c= seq (a,b2) )
thus  ( b1 <= b2 implies seq (a,b1) c= seq (a,b2) ) ::_thesis: ( seq (a,b1) c= seq (a,b2) implies b1 <= b2 )
proof
assume  b1 <= b2 ; ::_thesis: seq (a,b1) c= seq (a,b2)
then A1: b1 + a <= b2 + a by XREAL_1:6;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in seq (a,b1) or b in seq (a,b2) )
assume A2: b in seq (a,b1) ; ::_thesis: b in seq (a,b2)
reconsider c = b as Element of NAT by A2;
 c <= b1 + a by A2, Th1;
then A3: c <= b2 + a by A1, XXREAL_0:2;
 1 + a <= c by A2, Th1;
hence  b in seq (a,b2) by A3; ::_thesis: verum
end;
assume A4: seq (a,b1) c= seq (a,b2) ; ::_thesis: b1 <= b2
now__::_thesis:_(_b1_<>_0_implies_b1_<=_b2_)
assume  b1 <> 0 ; ::_thesis: b1 <= b2
then  b1 + a in seq (a,b1) by Th3;
then  b1 + a <= b2 + a by A4, Th1;
hence  b1 <= b2 by XREAL_1:6; ::_thesis: verum
end;
hence  b1 <= b2 ; ::_thesis: verum
end;

theorem Th5: :: CALCUL_2:5
for a, b being natural number holds (seq (a,b)) \/ {((a + b) + 1)} = seq (a,(b + 1))
proof
let a, b be natural number ; ::_thesis: (seq (a,b)) \/ {((a + b) + 1)} = seq (a,(b + 1))
thus  (seq (a,b)) \/ {((a + b) + 1)} c= seq (a,(b + 1)) :: according to XBOOLE_0:def_10 ::_thesis: seq (a,(b + 1)) c= (seq (a,b)) \/ {((a + b) + 1)}
proof
 b + 0 <= b + 1 by XREAL_1:7;
then A1: seq (a,b) c= seq (a,(b + 1)) by Th4;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (seq (a,b)) \/ {((a + b) + 1)} or x in seq (a,(b + 1)) )
assume  x in (seq (a,b)) \/ {((a + b) + 1)} ; ::_thesis: x in seq (a,(b + 1))
then  ( x in seq (a,b) or x in {((a + b) + 1)} ) by XBOOLE_0:def_3;
then  ( x in seq (a,(b + 1)) or x = a + (b + 1) ) by A1, TARSKI:def_1;
hence  x in seq (a,(b + 1)) by Th3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in seq (a,(b + 1)) or x in (seq (a,b)) \/ {((a + b) + 1)} )
assume A2: x in seq (a,(b + 1)) ; ::_thesis: x in (seq (a,b)) \/ {((a + b) + 1)}
reconsider x = x as Element of NAT by A2;
 x <= (b + 1) + a by A2, Th1;
then A3: ( x <= a + b or x = (a + b) + 1 ) by NAT_1:8;
 1 + a <= x by A2, Th1;
then  ( x in seq (a,b) or x in {((a + b) + 1)} ) by A3, TARSKI:def_1;
hence  x in (seq (a,b)) \/ {((a + b) + 1)} by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th6: :: CALCUL_2:6
for m, n being Element of NAT holds seq (m,n),n are_equipotent
proof
let m, n be Element of NAT ; ::_thesis: seq (m,n),n are_equipotent
defpred S1[ Element of NAT ] means  seq (m,$1),$1 are_equipotent ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: seq (m,n),n are_equipotent ; ::_thesis: S1[n + 1]
reconsider i = m + n as Element of NAT ;
A3: n + 1 = succ n by NAT_1:38
.= n \/ {n} by ORDINAL1:def_1 ;
A4: now__::_thesis:_not_seq_(m,n)_meets_{(i_+_1)}
assume  seq (m,n) meets {(i + 1)} ; ::_thesis: contradiction
then consider x being set  such that
A5: x in seq (m,n) and
A6: x in {(i + 1)} by XBOOLE_0:3;
A7: not i + 1 <= i by NAT_1:13;
 x = i + 1 by A6, TARSKI:def_1;
hence  contradiction by A5, A7, Th1; ::_thesis: verum
end;
A8: now__::_thesis:_not_n_meets_{n}
assume  n meets {n} ; ::_thesis: contradiction
then consider x being set  such that
A9: x in n and
A10: x in {n} by XBOOLE_0:3;
 x = n by A10, TARSKI:def_1;
hence  contradiction by A9; ::_thesis: verum
end;
 ( seq (m,(n + 1)) = (seq (m,n)) \/ {(i + 1)} & {(i + 1)},{n} are_equipotent ) by Th5, CARD_1:28;
hence  S1[n + 1] by A2, A3, A8, A4, CARD_1:31; ::_thesis: verum
end;
A11: S1[ 0 ] by Th2;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A11, A1);
hence  seq (m,n),n are_equipotent ; ::_thesis: verum
end;

registration
let m, n be Element of NAT ;
cluster seq (m,n) ->  finite ;
coherence
 seq (m,n) is finite
proof
 ( n is finite & n, seq (m,n) are_equipotent ) by Th6;
hence  seq (m,n) is finite by CARD_1:38; ::_thesis: verum
end;
end;

registration
let Al be QC-alphabet ;
let f be FinSequence of CQC-WFF Al;
cluster card f ->  finite ;
coherence
 len f is finite ;
end;

theorem Th7: :: CALCUL_2:7
for m, n being Element of NAT holds seq (m,n) c= Seg (m + n)
proof
let m, n be Element of NAT ; ::_thesis: seq (m,n) c= Seg (m + n)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in seq (m,n) or x in Seg (m + n) )
A1: 1 <= 1 + m by NAT_1:11;
assume A2: x in seq (m,n) ; ::_thesis: x in Seg (m + n)
then reconsider x = x as Element of NAT ;
 1 + m <= x by A2, Th1;
then A3: 1 <= x by A1, XXREAL_0:2;
 x <= n + m by A2, Th1;
hence  x in Seg (m + n) by A3, FINSEQ_1:1; ::_thesis: verum
end;

theorem :: CALCUL_2:8
for n, m being Element of NAT holds Seg n misses seq (n,m)
proof
let n, m be Element of NAT ; ::_thesis: Seg n misses seq (n,m)
assume  Seg n meets seq (n,m) ; ::_thesis: contradiction
then consider a being set  such that
A1: a in Seg n and
A2: a in seq (n,m) by XBOOLE_0:3;
reconsider i = a as Element of NAT by A1;
 ( i <= n & n + 1 <= i ) by A1, A2, Th1, FINSEQ_1:1;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;

theorem :: CALCUL_2:9
for f, g being FinSequence holds dom (f ^ g) = (dom f) \/ (seq ((len f),(len g)))
proof
let f, g be FinSequence; ::_thesis: dom (f ^ g) = (dom f) \/ (seq ((len f),(len g)))
now__::_thesis:_for_a_being_set_st_a_in_dom_(f_^_g)_holds_
a_in_(dom_f)_\/_(seq_((len_f),(len_g)))
let a be set ; ::_thesis: ( a in dom (f ^ g) implies b1 in (dom f) \/ (seq ((len f),(len g))) )
assume A1: a in dom (f ^ g) ; ::_thesis: b1 in (dom f) \/ (seq ((len f),(len g)))
reconsider i = a as Element of NAT by A1;
A2: 1 <= i by A1, FINSEQ_3:25;
A3: i <= len (f ^ g) by A1, FINSEQ_3:25;
percases ( i <= len f or len f < i ) ;
supposeA4: i <= len f ; ::_thesis: b1 in (dom f) \/ (seq ((len f),(len g)))
A5: dom f c= (dom f) \/ (seq ((len f),(len g))) by XBOOLE_1:7;
 i in dom f by A2, A4, FINSEQ_3:25;
hence  a in (dom f) \/ (seq ((len f),(len g))) by A5; ::_thesis: verum
end;
supposeA6: len f < i ; ::_thesis: b1 in (dom f) \/ (seq ((len f),(len g)))
A7: seq ((len f),(len g)) c= (dom f) \/ (seq ((len f),(len g))) by XBOOLE_1:7;
A8: i <= (len f) + (len g) by A3, FINSEQ_1:22;
 (len f) + 1 <= i by A6, NAT_1:13;
then  a in seq ((len f),(len g)) by A8;
hence  a in (dom f) \/ (seq ((len f),(len g))) by A7; ::_thesis: verum
end;
end;
end;
hence  dom (f ^ g) c= (dom f) \/ (seq ((len f),(len g))) by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: (dom f) \/ (seq ((len f),(len g))) c= dom (f ^ g)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (dom f) \/ (seq ((len f),(len g))) or a in dom (f ^ g) )
assume A9: a in (dom f) \/ (seq ((len f),(len g))) ; ::_thesis: a in dom (f ^ g)
percases ( a in dom f or a in seq ((len f),(len g)) ) by A9, XBOOLE_0:def_3;
supposeA10: a in dom f ; ::_thesis: a in dom (f ^ g)
then reconsider i = a as Element of NAT ;
A11: 1 <= i by A10, FINSEQ_3:25;
A12: len f <= len (f ^ g) by CALCUL_1:6;
 i <= len f by A10, FINSEQ_3:25;
then  i <= len (f ^ g) by A12, XXREAL_0:2;
hence  a in dom (f ^ g) by A11, FINSEQ_3:25; ::_thesis: verum
end;
supposeA13: a in seq ((len f),(len g)) ; ::_thesis: a in dom (f ^ g)
then reconsider i = a as Element of NAT ;
 i <= (len g) + (len f) by A13, Th1;
then A14: i <= len (f ^ g) by FINSEQ_1:22;
A15: 1 <= 1 + (len f) by NAT_1:11;
 1 + (len f) <= i by A13, Th1;
then  1 <= i by A15, XXREAL_0:2;
hence  a in dom (f ^ g) by A14, FINSEQ_3:25; ::_thesis: verum
end;
end;
end;

theorem Th10: :: CALCUL_2:10
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds len (Sgm (seq ((len g),(len f)))) = len f
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds len (Sgm (seq ((len g),(len f)))) = len f
let g, f be FinSequence of CQC-WFF Al; ::_thesis: len (Sgm (seq ((len g),(len f)))) = len f
 seq ((len g),(len f)), len f are_equipotent by Th6;
then A1: card (seq ((len g),(len f))) = card (len f) by CARD_1:5;
 seq ((len g),(len f)) c= Seg ((len g) + (len f)) by Th7;
hence  len (Sgm (seq ((len g),(len f)))) = len f by A1, FINSEQ_3:39; ::_thesis: verum
end;

theorem Th11: :: CALCUL_2:11
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds dom (Sgm (seq ((len g),(len f)))) = dom f
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds dom (Sgm (seq ((len g),(len f)))) = dom f
let g, f be FinSequence of CQC-WFF Al; ::_thesis: dom (Sgm (seq ((len g),(len f)))) = dom f
 len (Sgm (seq ((len g),(len f)))) = len f by Th10;
hence  dom (Sgm (seq ((len g),(len f)))) = dom f by FINSEQ_3:29; ::_thesis: verum
end;

theorem Th12: :: CALCUL_2:12
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))
let g, f be FinSequence of CQC-WFF Al; ::_thesis: rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))
 seq ((len g),(len f)) c= Seg ((len g) + (len f)) by Th7;
hence  rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f)) by FINSEQ_1:def_13; ::_thesis: verum
end;

theorem Th13: :: CALCUL_2:13
for Al being QC-alphabet
for i being Element of NAT
for g, f being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
proof
let Al be QC-alphabet ; ::_thesis: for i being Element of NAT
for g, f being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
let i be Element of NAT ; ::_thesis: for g, f being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
let g, f be FinSequence of CQC-WFF Al; ::_thesis: ( i in dom (Sgm (seq ((len g),(len f)))) implies (Sgm (seq ((len g),(len f)))) . i = (len g) + i )
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies for i being Element of NAT st 1 <= i & i <= $1 holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i );
assume A1: i in dom (Sgm (seq ((len g),(len f)))) ; ::_thesis: (Sgm (seq ((len g),(len f)))) . i = (len g) + i
then  i in dom f by Th11;
then A2: i <= len f by FINSEQ_3:25;
A3: 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 A4: S1[k] ; ::_thesis: S1[k + 1]
assume that
A5: 1 <= k + 1 and
A6: k + 1 <= len f ; ::_thesis: for i being Element of NAT st 1 <= i & i <= k + 1 holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= k + 1 implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n )
assume that
A7: 1 <= n and
A8: n <= k + 1 ; ::_thesis: (Sgm (seq ((len g),(len f)))) . n = (len g) + n
A9: now__::_thesis:_(_n_=_k_+_1_implies_(Sgm_(seq_((len_g),(len_f))))_._n_=_(len_g)_+_n_)
assume A10: n = k + 1 ; ::_thesis: (Sgm (seq ((len g),(len f)))) . n = (len g) + n
 dom (Sgm (seq ((len g),(len f)))) = dom f by Th11;
then  n in dom (Sgm (seq ((len g),(len f)))) by A5, A6, A10, FINSEQ_3:25;
then  (Sgm (seq ((len g),(len f)))) . n in rng (Sgm (seq ((len g),(len f)))) by FUNCT_1:3;
then reconsider i = (Sgm (seq ((len g),(len f)))) . n as Element of NAT ;
A11: now__::_thesis:_not_i_<_(len_g)_+_(k_+_1)
assume A12: i < (len g) + (k + 1) ; ::_thesis: contradiction
A13: now__::_thesis:_not_k_<>_0
assume  k <> 0 ; ::_thesis: contradiction
then A14: 0 + 1 <= k by NAT_1:13;
then A15: (Sgm (seq ((len g),(len f)))) . k = (len g) + k by A4, A6, NAT_1:13;
then reconsider j = (Sgm (seq ((len g),(len f)))) . k as Element of NAT ;
A16: seq ((len g),(len f)) c= Seg ((len g) + (len f)) by Th7;
A17: ( k < k + 1 & k + 1 <= len (Sgm (seq ((len g),(len f)))) ) by A6, Th10, NAT_1:13;
 i < ((len g) + k) + 1 by A12;
then  i <= j by A15, NAT_1:13;
hence  contradiction by A10, A14, A17, A16, FINSEQ_1:def_13; ::_thesis: verum
end;
now__::_thesis:_not_k_=_0
 1 <= len f by A5, A6, XXREAL_0:2;
then  1 in dom f by FINSEQ_3:25;
then A18: 1 in dom (Sgm (seq ((len g),(len f)))) by Th11;
assume A19: k = 0 ; ::_thesis: contradiction
then  not i in seq ((len g),(len f)) by A12, Th1;
then  not i in rng (Sgm (seq ((len g),(len f)))) by Th12;
hence  contradiction by A10, A19, A18, FUNCT_1:3; ::_thesis: verum
end;
hence  contradiction by A13; ::_thesis: verum
end;
now__::_thesis:_not_i_>_(len_g)_+_(k_+_1)
 ( 1 + (len g) <= (1 + (len g)) + k & (len g) + (k + 1) <= (len f) + (len g) ) by A6, NAT_1:11, XREAL_1:6;
then  (len g) + (k + 1) in seq ((len g),(len f)) ;
then  (len g) + (k + 1) in rng (Sgm (seq ((len g),(len f)))) by Th12;
then consider l being Nat such that
A20: l in dom (Sgm (seq ((len g),(len f)))) and
A21: (Sgm (seq ((len g),(len f)))) . l = (len g) + (k + 1) by FINSEQ_2:10;
assume A22: i > (len g) + (k + 1) ; ::_thesis: contradiction
A23: now__::_thesis:_not_l_<=_k_+_1
A24: now__::_thesis:_not_l_<=_k
assume A25: l <= k ; ::_thesis: contradiction
now__::_thesis:_not_1_<=_l
assume  1 <= l ; ::_thesis: contradiction
then  (len g) + (k + 1) = (len g) + l by A4, A6, A20, A21, A25, NAT_1:13, XXREAL_0:2;
hence  contradiction by A25, NAT_1:13; ::_thesis: verum
end;
hence  contradiction by A20, FINSEQ_3:25; ::_thesis: verum
end;
assume  l <= k + 1 ; ::_thesis: contradiction
hence  contradiction by A10, A22, A21, A24, NAT_1:8; ::_thesis: verum
end;
A26: ( 1 <= n & seq ((len g),(len f)) c= Seg ((len g) + (len f)) ) by A10, Th7, NAT_1:11;
 l <= len (Sgm (seq ((len g),(len f)))) by A20, FINSEQ_3:25;
hence  contradiction by A10, A22, A21, A23, A26, FINSEQ_1:def_13; ::_thesis: verum
end;
hence  (Sgm (seq ((len g),(len f)))) . n = (len g) + n by A10, A11, XXREAL_0:1; ::_thesis: verum
end;
 ( n <= k implies (Sgm (seq ((len g),(len f)))) . n = (len g) + n ) by A4, A6, A7, NAT_1:13, XXREAL_0:2;
hence  (Sgm (seq ((len g),(len f)))) . n = (len g) + n by A8, A9, NAT_1:8; ::_thesis: verum
end;
A27: S1[ 0 ] ;
A28: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A27, A3);
 1 <= i by A1, FINSEQ_3:25;
hence  (Sgm (seq ((len g),(len f)))) . i = (len g) + i by A2, A28; ::_thesis: verum
end;

theorem Th14: :: CALCUL_2:14
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds seq ((len g),(len f)) c= dom (g ^ f)
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds seq ((len g),(len f)) c= dom (g ^ f)
let g, f be FinSequence of CQC-WFF Al; ::_thesis: seq ((len g),(len f)) c= dom (g ^ f)
now__::_thesis:_for_a_being_set_st_a_in_seq_((len_g),(len_f))_holds_
a_in_dom_(g_^_f)
let a be set ; ::_thesis: ( a in seq ((len g),(len f)) implies a in dom (g ^ f) )
assume A1: a in seq ((len g),(len f)) ; ::_thesis: a in dom (g ^ f)
reconsider n = a as Element of NAT by A1;
 n <= (len f) + (len g) by A1, Th1;
then A2: n <= len (g ^ f) by FINSEQ_1:22;
A3: 1 <= 1 + (len g) by NAT_1:11;
 1 + (len g) <= n by A1, Th1;
then  1 <= n by A3, XXREAL_0:2;
hence  a in dom (g ^ f) by A2, FINSEQ_3:25; ::_thesis: verum
end;
hence  seq ((len g),(len f)) c= dom (g ^ f) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th15: :: CALCUL_2:15
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))
let g, f be FinSequence of CQC-WFF Al; ::_thesis: dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))
 dom ((g ^ f) | (seq ((len g),(len f)))) = (dom (g ^ f)) /\ (seq ((len g),(len f))) by RELAT_1:61;
hence  dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f)) by Th14, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th16: :: CALCUL_2:16
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)
let g, f be FinSequence of CQC-WFF Al; ::_thesis: Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)
reconsider gf = (g ^ f) | (seq ((len g),(len f))) as FinSubsequence ;
Seq gf = gf * (Sgm (dom gf)) by FINSEQ_1:def_14
.= gf * (Sgm (seq ((len g),(len f)))) by Th15
.= ((g ^ f) | (rng (Sgm (seq ((len g),(len f)))))) * (Sgm (seq ((len g),(len f)))) by Th12
.= (g ^ f) * (Sgm (seq ((len g),(len f)))) by FUNCT_4:2 ;
hence  Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f) ; ::_thesis: verum
end;

theorem Th17: :: CALCUL_2:17
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al holds dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al holds dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
let g, f be FinSequence of CQC-WFF Al; ::_thesis: dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f
 rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f)) by Th12;
then A1: rng (Sgm (seq ((len g),(len f)))) c= dom (g ^ f) by Th14;
 dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom ((Sgm (seq ((len g),(len f)))) * (g ^ f)) by Th16;
then  dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom (Sgm (seq ((len g),(len f)))) by A1, RELAT_1:27;
hence  dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f by Th11; ::_thesis: verum
end;

theorem Th18: :: CALCUL_2:18
for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of g ^ f
proof
let Al be QC-alphabet ; ::_thesis: for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of g ^ f
let f, g be FinSequence of CQC-WFF Al; ::_thesis: f is_Subsequence_of g ^ f
A1: for i being Nat st i in dom (Seq ((g ^ f) | (seq ((len g),(len f))))) holds
(Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i
proof
let i be Nat; ::_thesis: ( i in dom (Seq ((g ^ f) | (seq ((len g),(len f))))) implies (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i )
assume  i in dom (Seq ((g ^ f) | (seq ((len g),(len f))))) ; ::_thesis: (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i
then A2: i in dom f by Th17;
then A3: i in dom (Sgm (seq ((len g),(len f)))) by Th11;
 (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = ((Sgm (seq ((len g),(len f)))) * (g ^ f)) . i by Th16;
then  (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = (g ^ f) . ((Sgm (seq ((len g),(len f)))) . i) by A3, FUNCT_1:13;
then  (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = (g ^ f) . ((len g) + i) by A3, Th13;
hence  (Seq ((g ^ f) | (seq ((len g),(len f))))) . i = f . i by A2, FINSEQ_1:def_7; ::_thesis: verum
end;
 dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f by Th17;
then  Seq ((g ^ f) | (seq ((len g),(len f)))) = f by A1, FINSEQ_1:13;
hence  f is_Subsequence_of g ^ f by CALCUL_1:def_4; ::_thesis: verum
end;

definition
let D be non empty set ;
let f be FinSequence of D;
let P be Permutation of (dom f);
func Per (f,P) ->  FinSequence of D equals :: CALCUL_2:def 2
P * f;
coherence
 P * f is FinSequence of D
proof
A1: rng P = dom f by FUNCT_2:def_3;
then  dom (P * f) = dom P by RELAT_1:27;
then  dom (P * f) = dom f by FUNCT_2:52;
then  ex n being Nat st dom (P * f) = Seg n by FINSEQ_1:def_2;
then reconsider F = P * f as FinSequence by FINSEQ_1:def_2;
 rng F = rng f by A1, RELAT_1:28;
hence  P * f is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines Per CALCUL_2:def_2_:_
 for D being non empty set
for f being FinSequence of D
for P being Permutation of (dom f) holds Per (f,P) = P * f;

theorem Th19: :: CALCUL_2:19
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f
proof
let Al be QC-alphabet ; ::_thesis: for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f
let f be FinSequence of CQC-WFF Al; ::_thesis: for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f
let P be Permutation of (dom f); ::_thesis: dom (Per (f,P)) = dom f
 rng P = dom f by FUNCT_2:def_3;
then  dom (P * f) = dom P by RELAT_1:27;
hence  dom (Per (f,P)) = dom f by FUNCT_2:52; ::_thesis: verum
end;

theorem Th20: :: CALCUL_2:20
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds
|- (g ^ f) ^ <*p*>
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds
|- (g ^ f) ^ <*p*>
let p be Element of CQC-WFF Al; ::_thesis: for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds
|- (g ^ f) ^ <*p*>
let f, g be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*p*> implies |- (g ^ f) ^ <*p*> )
 Suc (f ^ <*p*>) = p by CALCUL_1:5;
then A1: Suc (f ^ <*p*>) = Suc ((g ^ f) ^ <*p*>) by CALCUL_1:5;
 Ant (f ^ <*p*>) = f by CALCUL_1:5;
then  Ant (f ^ <*p*>) is_Subsequence_of g ^ f by Th18;
then A2: Ant (f ^ <*p*>) is_Subsequence_of Ant ((g ^ f) ^ <*p*>) by CALCUL_1:5;
assume  |- f ^ <*p*> ; ::_thesis: |- (g ^ f) ^ <*p*>
hence  |- (g ^ f) ^ <*p*> by A2, A1, CALCUL_1:36; ::_thesis: verum
end;

begin

definition
let Al be QC-alphabet ;
let f be FinSequence of CQC-WFF Al;
func Begin f ->  Element of CQC-WFF Al means :Def3: :: CALCUL_2:def 3
it = f . 1 if 1 <= len f
otherwise it = VERUM Al;
existence
 ( ( 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = f . 1 ) & ( not 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = VERUM Al ) )
proof
 ( 1 <= len f implies ex p being Element of CQC-WFF Al st p = f . 1 )
proof
assume  1 <= len f ; ::_thesis: ex p being Element of CQC-WFF Al st p = f . 1
then  1 in dom f by FINSEQ_3:25;
then  f . 1 in CQC-WFF Al by FINSEQ_2:11;
hence  ex p being Element of CQC-WFF Al st p = f . 1 ; ::_thesis: verum
end;
hence  ( ( 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = f . 1 ) & ( not 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = VERUM Al ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of CQC-WFF Al holds
( ( 1 <= len f & b1 = f . 1 & b2 = f . 1 implies b1 = b2 ) & ( not 1 <= len f & b1 = VERUM Al & b2 = VERUM Al implies b1 = b2 ) ) ;
consistency
 for b1 being Element of CQC-WFF Al holds verum ;
end;

:: deftheorem Def3 defines Begin CALCUL_2:def_3_:_
 for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al
for b3 being Element of CQC-WFF Al holds
( ( 1 <= len f implies ( b3 = Begin f iff b3 = f . 1 ) ) & ( not 1 <= len f implies ( b3 = Begin f iff b3 = VERUM Al ) ) );

definition
let Al be QC-alphabet ;
let f be FinSequence of CQC-WFF Al;
assume A1: 1 <= len f ;
func Impl f ->  Element of CQC-WFF Al means :Def4: :: CALCUL_2:def 4
 ex F being FinSequence of CQC-WFF Al st
( it = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) );
existence
 ex b1 being Element of CQC-WFF Al ex F being FinSequence of CQC-WFF Al st
( b1 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) )
proof
defpred S1[ Element of NAT , set , set ] means  ex p, q being Element of CQC-WFF Al st
( p = f . ($1 + 1) & q = $2 & $3 = p => q );
A2: for n being Element of NAT st 1 <= n & n < len f holds
for x being Element of CQC-WFF Al ex y being Element of CQC-WFF Al st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len f implies for x being Element of CQC-WFF Al ex y being Element of CQC-WFF Al st S1[n,x,y] )
assume that
 1 <= n and
A3: n < len f ; ::_thesis: for x being Element of CQC-WFF Al ex y being Element of CQC-WFF Al st S1[n,x,y]
 ( 1 <= n + 1 & n + 1 <= len f ) by A3, NAT_1:11, NAT_1:13;
then  n + 1 in dom f by FINSEQ_3:25;
then reconsider p = f . (n + 1) as Element of CQC-WFF Al by FINSEQ_2:11;
let x be Element of CQC-WFF Al; ::_thesis: ex y being Element of CQC-WFF Al st S1[n,x,y]
take  p => x ; ::_thesis: S1[n,x,p => x]
take  p ; ::_thesis: ex q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = x & p => x = p => q )
take  x ; ::_thesis: ( p = f . (n + 1) & x = x & p => x = p => x )
thus  ( p = f . (n + 1) & x = x & p => x = p => x ) ; ::_thesis: verum
end;
consider F being FinSequence of CQC-WFF Al such that
A4: ( len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_4(A2);
 len f in dom F by A1, A4, FINSEQ_3:25;
then reconsider p = F . (len f) as Element of CQC-WFF Al by FINSEQ_2:11;
take  p ; ::_thesis: ex F being FinSequence of CQC-WFF Al st
( p = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) )
thus  ex F being FinSequence of CQC-WFF Al st
( p = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of CQC-WFF Al st ex F being FinSequence of CQC-WFF Al st
( b1 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) & ex F being FinSequence of CQC-WFF Al st
( b2 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) holds
b1 = b2
proof
defpred S1[ Element of NAT , set , set ] means  ex p, q being Element of CQC-WFF Al st
( p = f . ($1 + 1) & q = $2 & $3 = p => q );
let p1, p2 be Element of CQC-WFF Al; ::_thesis: ( ex F being FinSequence of CQC-WFF Al st
( p1 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) & ex F being FinSequence of CQC-WFF Al st
( p2 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) implies p1 = p2 )
assume that
A5: ex F being FinSequence of CQC-WFF Al st
( p1 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
S1[n,F . n,F . (n + 1)] ) ) and
A6: ex F being FinSequence of CQC-WFF Al st
( p2 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
S1[n,F . n,F . (n + 1)] ) ) ; ::_thesis: p1 = p2
consider H being FinSequence of CQC-WFF Al such that
A7: p2 = H . (len f) and
A8: ( len H = len f & ( H . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
S1[n,H . n,H . (n + 1)] ) ) by A6;
consider G being FinSequence of CQC-WFF Al such that
A9: p1 = G . (len f) and
A10: ( len G = len f & ( G . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
S1[n,G . n,G . (n + 1)] ) ) by A5;
A11: for n being Element of NAT st 1 <= n & n < len f holds
for x, y1, y2 being Element of CQC-WFF Al st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2 ;
 G = H from RECDEF_1:sch_8(A11, A10, A8);
hence  p1 = p2 by A9, A7; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Impl CALCUL_2:def_4_:_
 for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al st 1 <= len f holds
for b3 being Element of CQC-WFF Al holds
( b3 = Impl f iff ex F being FinSequence of CQC-WFF Al st
( b3 = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Element of NAT st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) );

theorem Th21: :: CALCUL_2:21
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>
proof
let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>
let p be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>
let f be FinSequence of CQC-WFF Al; ::_thesis: |- (f ^ <*p*>) ^ <*p*>
 len (f ^ <*p*>) in dom (f ^ <*p*>) by CALCUL_1:10;
then  (len f) + (len <*p*>) in dom (f ^ <*p*>) by FINSEQ_1:22;
then A1: (len f) + 1 in dom (f ^ <*p*>) by FINSEQ_1:39;
 (f ^ <*p*>) . ((len f) + 1) = p by FINSEQ_1:42;
then  p is_tail_of f ^ <*p*> by A1, CALCUL_1:def_16;
then  Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of f ^ <*p*> by CALCUL_1:5;
then  Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p*>) by CALCUL_1:5;
hence  |- (f ^ <*p*>) ^ <*p*> by CALCUL_1:33; ::_thesis: verum
end;

theorem Th22: :: CALCUL_2:22
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*p*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*p*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*p*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*(p '&' q)*> implies |- f ^ <*p*> )
A1: p '&' q = Suc (f ^ <*(p '&' q)*>) by CALCUL_1:5;
assume  |- f ^ <*(p '&' q)*> ; ::_thesis: |- f ^ <*p*>
then  |- (Ant (f ^ <*(p '&' q)*>)) ^ <*p*> by A1, CALCUL_1:40;
hence  |- f ^ <*p*> by CALCUL_1:5; ::_thesis: verum
end;

theorem Th23: :: CALCUL_2:23
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*q*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*(p '&' q)*> implies |- f ^ <*q*> )
A1: p '&' q = Suc (f ^ <*(p '&' q)*>) by CALCUL_1:5;
assume  |- f ^ <*(p '&' q)*> ; ::_thesis: |- f ^ <*q*>
then  |- (Ant (f ^ <*(p '&' q)*>)) ^ <*q*> by A1, CALCUL_1:41;
hence  |- f ^ <*q*> by CALCUL_1:5; ::_thesis: verum
end;

theorem Th24: :: CALCUL_2:24
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*q*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> implies |- f ^ <*q*> )
A1: 1 <= len (f ^ <*p*>) by CALCUL_1:10;
assume  ( |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> ) ; ::_thesis: |- f ^ <*q*>
then  |- (Ant (f ^ <*p*>)) ^ <*q*> by A1, CALCUL_1:45;
hence  |- f ^ <*q*> by CALCUL_1:5; ::_thesis: verum
end;

theorem Th25: :: CALCUL_2:25
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- f ^ <*('not' p)*> holds
|- f ^ <*q*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- f ^ <*('not' p)*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- f ^ <*('not' p)*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*p*> & |- f ^ <*('not' p)*> implies |- f ^ <*q*> )
A1: ( Ant (f ^ <*p*>) = f & Suc (f ^ <*p*>) = p ) by CALCUL_1:5;
assume  ( |- f ^ <*p*> & |- f ^ <*('not' p)*> ) ; ::_thesis: |- f ^ <*q*>
hence  |- f ^ <*q*> by A1, CALCUL_1:44; ::_thesis: verum
end;

theorem Th26: :: CALCUL_2:26
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> implies |- f ^ <*q*> )
set f1 = (f ^ <*p*>) ^ <*q*>;
set f2 = (f ^ <*('not' p)*>) ^ <*q*>;
assume A1: ( |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> ) ; ::_thesis: |- f ^ <*q*>
A2: Ant ((f ^ <*('not' p)*>) ^ <*q*>) = f ^ <*('not' p)*> by CALCUL_1:5;
A3: Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*> by CALCUL_1:5;
then  Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p by CALCUL_1:5;
then A4: 'not' (Suc (Ant ((f ^ <*p*>) ^ <*q*>))) = Suc (Ant ((f ^ <*('not' p)*>) ^ <*q*>)) by A2, CALCUL_1:5;
A5: ( 1 < len ((f ^ <*p*>) ^ <*q*>) & 1 < len ((f ^ <*('not' p)*>) ^ <*q*>) ) by CALCUL_1:9;
A6: Suc ((f ^ <*p*>) ^ <*q*>) = q by CALCUL_1:5;
then A7: Suc ((f ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*('not' p)*>) ^ <*q*>) by CALCUL_1:5;
A8: Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f by A3, CALCUL_1:5;
then  Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = Ant (Ant ((f ^ <*('not' p)*>) ^ <*q*>)) by A2, CALCUL_1:5;
hence  |- f ^ <*q*> by A1, A8, A4, A6, A5, A7, CALCUL_1:37; ::_thesis: verum
end;

theorem Th27: :: CALCUL_2:27
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*(p => q)*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*(p => q)*>
let p, q be Element of CQC-WFF Al; ::_thesis: for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*(p => q)*>
let f be FinSequence of CQC-WFF Al; ::_thesis: ( |- (f ^ <*p*>) ^ <*q*> implies |- f ^ <*(p => q)*> )
assume A1: |- (f ^ <*p*>) ^ <*q*> ; ::_thesis: |- f ^ <*(p => q)*>
set g1 = ((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>;
set g = (f ^ <*p*>) ^ <*q*>;
A2: Ant (((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) = (f ^ <*(p '&' ('not' q))*>) ^ <*p*> by CALCUL_1:5;
 Suc ((f ^ <*p*>) ^ <*q*>) = q by CALCUL_1:5;
then A3: Suc (((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*p*>) ^ <*q*>) by CALCUL_1:5;
A4: Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*> by CALCUL_1:5;
then A5: 0 + 1 <= len (Ant ((f ^ <*p*>) ^ <*q*>)) by CALCUL_1:10;
A6: |- (f ^ <*(p '&' ('not' q))*>) ^ <*(p '&' ('not' q))*> by Th21;
then A7: |- (f ^ <*(p '&' ('not' q))*>) ^ <*p*> by Th22;
 ( Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f & Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p ) by A4, CALCUL_1:5;
then  |- ((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*> by A1, A5, A3, A2, CALCUL_1:13, CALCUL_1:36;
then A8: |- (f ^ <*(p '&' ('not' q))*>) ^ <*q*> by A7, Th24;
A9: |- (f ^ <*('not' (p '&' ('not' q)))*>) ^ <*('not' (p '&' ('not' q)))*> by Th21;
 |- (f ^ <*(p '&' ('not' q))*>) ^ <*('not' q)*> by A6, Th23;
then  |- (f ^ <*(p '&' ('not' q))*>) ^ <*('not' (p '&' ('not' q)))*> by A8, Th25;
then  |- f ^ <*('not' (p '&' ('not' q)))*> by A9, Th26;
hence  |- f ^ <*(p => q)*> by QC_LANG2:def_2; ::_thesis: verum
end;

theorem Th28: :: CALCUL_2:28
for Al being QC-alphabet
for g, f being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds
|- f ^ <*(Impl (Rev g))*>
proof
let Al be QC-alphabet ; ::_thesis: for g, f being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds
|- f ^ <*(Impl (Rev g))*>
let g, f be FinSequence of CQC-WFF Al; ::_thesis: ( 1 <= len g & |- f ^ g implies |- f ^ <*(Impl (Rev g))*> )
set h = Rev g;
assume that
A1: 1 <= len g and
A2: |- f ^ g ; ::_thesis: |- 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 Element of 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[ Element of 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 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 A10: S1[k] ; ::_thesis: 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 ; ::_thesis: 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__::_thesis:_(_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 ; ::_thesis: 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; ::_thesis: verum
end;
A32: k + 1 <= len (f ^ g) by A14, A11, XXREAL_0:2;
now__::_thesis:_(_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 ; ::_thesis: 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: verum
end;
A38: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(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; ::_thesis: verum
end;

theorem Th29: :: CALCUL_2:29
for Al being 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*>
proof
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 Element of 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[ Element of 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 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 A10: S1[k] ; ::_thesis: S1[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*> )
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*>_)_)
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 Element of 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 set  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;
now__::_thesis:_(_k_=_0_implies_ex_p,_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;
hence  ex p being Element of CQC-WFF Al st
( p = (Rev F) . (k + 1) & |- (Per (f,P)) ^ <*p*> ) by A13; ::_thesis: verum
end;
A37: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(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
end;

theorem :: CALCUL_2:30
for Al being 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 |- f ^ <*p*> holds
|- (Per (f,P)) ^ <*p*>
proof
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 |- 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 |- f ^ <*p*> holds
|- (Per (f,P)) ^ <*p*>
let f be FinSequence of CQC-WFF Al; ::_thesis: for P being Permutation of (dom f) st |- f ^ <*p*> holds
|- (Per (f,P)) ^ <*p*>
let P be Permutation of (dom f); ::_thesis: ( |- f ^ <*p*> implies |- (Per (f,P)) ^ <*p*> )
set g = f ^ <*p*>;
assume  |- f ^ <*p*> ; ::_thesis: |- (Per (f,P)) ^ <*p*>
then  |- ((Per (f,P)) ^ f) ^ <*p*> by Th20;
then A1: |- (Per (f,P)) ^ (f ^ <*p*>) by FINSEQ_1:32;
 1 <= len (f ^ <*p*>) by CALCUL_1:10;
then  |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> by A1, Th28;
hence  |- (Per (f,P)) ^ <*p*> by Th29; ::_thesis: verum
end;

begin

notation
let n be Element of NAT ;
let c be set ;
synonym  IdFinS (c,n) for n |-> c;
end;

theorem Th31: :: CALCUL_2:31
for n being Element of NAT
for c being set st 1 <= n holds
rng (IdFinS (c,n)) = rng <*c*>
proof
let n be Element of NAT ; ::_thesis: for c being set st 1 <= n holds
rng (IdFinS (c,n)) = rng <*c*>
let c be set ; ::_thesis: ( 1 <= n implies rng (IdFinS (c,n)) = rng <*c*> )
assume A1: 1 <= n ; ::_thesis: rng (IdFinS (c,n)) = rng <*c*>
 n in Seg n by A1, FINSEQ_1:1;
then A2: (IdFinS (c,n)) . n = c by FUNCOP_1:7;
thus  rng (IdFinS (c,n)) c= rng <*c*> :: according to XBOOLE_0:def_10 ::_thesis: rng <*c*> c= rng (IdFinS (c,n))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng (IdFinS (c,n)) or a in rng <*c*> )
assume  a in rng (IdFinS (c,n)) ; ::_thesis: a in rng <*c*>
then consider i being Nat such that
A3: i in dom (IdFinS (c,n)) and
A4: (IdFinS (c,n)) . i = a by FINSEQ_2:10;
 i in Seg (len (IdFinS (c,n))) by A3, FINSEQ_1:def_3;
then  i in Seg n by CARD_1:def_7;
then  a = c by A4, FUNCOP_1:7;
then  a in {c} by TARSKI:def_1;
hence  a in rng <*c*> by FINSEQ_1:38; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng <*c*> or a in rng (IdFinS (c,n)) )
assume  a in rng <*c*> ; ::_thesis: a in rng (IdFinS (c,n))
then  a in {c} by FINSEQ_1:38;
then A5: a = c by TARSKI:def_1;
 n = len (IdFinS (c,n)) by CARD_1:def_7;
then  n in dom (IdFinS (c,n)) by A1, FINSEQ_3:25;
hence  a in rng (IdFinS (c,n)) by A5, A2, FUNCT_1:def_3; ::_thesis: verum
end;

definition
let D be non empty set ;
let n be Element of NAT ;
let p be Element of D;
:: original: IdFinS
redefine func IdFinS (p,n) ->  FinSequence of D;
coherence
 IdFinS (p,n) is FinSequence of D
proof
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(IdFinS_(p,n))_holds_
(IdFinS_(p,n))_._i_in_D
let i be Nat; ::_thesis: ( i in dom (IdFinS (p,n)) implies (IdFinS (p,n)) . i in D )
assume  i in dom (IdFinS (p,n)) ; ::_thesis: (IdFinS (p,n)) . i in D
then  i in Seg (len (IdFinS (p,n))) by FINSEQ_1:def_3;
then  i in Seg n by CARD_1:def_7;
then  (IdFinS (p,n)) . i = p by FUNCOP_1:7;
hence  (IdFinS (p,n)) . i in D ; ::_thesis: verum
end;
hence  IdFinS (p,n) is FinSequence of D by FINSEQ_2:12; ::_thesis: verum
end;
end;

theorem :: CALCUL_2:32
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for n being Element of NAT
for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
proof
let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al
for n being Element of NAT
for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
let p, q be Element of CQC-WFF Al; ::_thesis: for n being Element of NAT
for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
let n be Element of NAT ; ::_thesis: for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>
let f be FinSequence of CQC-WFF Al; ::_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 Element of 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 S1[ Element of 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 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 A12: S1[k] ; ::_thesis: S1[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 ;
then reconsider j = (len ((f ^ (IdFinS (p,n))) ^ <*q*>)) - i as Element of NAT ;
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  j < (len (f ^ (IdFinS (p,n)))) + (len <*q*>) by FINSEQ_1:22;
then  j < (len (f ^ (IdFinS (p,n)))) + 1 by FINSEQ_1:39;
then  j <= len (f ^ (IdFinS (p,n))) by NAT_1:13;
then A30: j in dom (f ^ (IdFinS (p,n))) by A22, A18, FINSEQ_3:25;
then A31: ((f ^ (IdFinS (p,n))) ^ <*q*>) . j = (((f ^ (IdFinS (p,n))) ^ <*q*>) | (dom (f ^ (IdFinS (p,n))))) . j by FUNCT_1:49;
A32: (f ^ (IdFinS (p,n))) . j 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))) . j 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))) . j by A31, FINSEQ_1:21;
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: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(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
end;