:: FINSEQ_6 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let x, y, z be set ;
cluster <*x,y,z*> -> non trivial ;
coherence
not <*x,y,z*> is trivial
proof end;
end;

registration
let f be non empty FinSequence;
cluster Rev f -> non empty ;
coherence
not Rev f is empty
proof end;
end;

Lm1: for x, y being set holds rng <*x,y*> = {x,y}
proof end;

Lm2: for x, y, z being set holds rng <*x,y,z*> = {x,y,z}
proof end;

theorem :: FINSEQ_6:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSEQ_6:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: FINSEQ_6:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for i being Nat st X c= Seg i & 1 in X holds
(Sgm X) . 1 = 1
proof end;

theorem Th4: :: FINSEQ_6:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for f being FinSequence st k in dom f & ( for i being Nat st 1 <= i & i < k holds
f . i <> f . k ) holds
(f . k) .. f = k
proof end;

theorem Th5: :: FINSEQ_6:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being set holds <*p1,p2*> | (Seg 1) = <*p1*>
proof end;

theorem Th6: :: FINSEQ_6:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 1) = <*p1*>
proof end;

theorem Th7: :: FINSEQ_6:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 2) = <*p1,p2*>
proof end;

theorem Th8: :: FINSEQ_6:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for p being set st p in rng f1 holds
p .. (f1 ^ f2) = p .. f1
proof end;

theorem Th9: :: FINSEQ_6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f2, f1 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
p .. (f1 ^ f2) = (len f1) + (p .. f2)
proof end;

theorem Th10: :: FINSEQ_6:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for p being set st p in rng f1 holds
(f1 ^ f2) |-- p = (f1 |-- p) ^ f2
proof end;

theorem Th11: :: FINSEQ_6:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f2, f1 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) |-- p = f2 |-- p
proof end;

theorem Th12: :: FINSEQ_6:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence holds f1 c= f1 ^ f2
proof end;

theorem Th13: :: FINSEQ_6:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for A being set st A c= dom f1 holds
(f1 ^ f2) | A = f1 | A
proof end;

theorem Th14: :: FINSEQ_6:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for p being set st p in rng f1 holds
(f1 ^ f2) -| p = f1 -| p
proof end;

registration
let f1 be FinSequence;
let i be natural number ;
cluster f1 | (Seg i) -> FinSequence-like ;
coherence
f1 | (Seg i) is FinSequence-like
by FINSEQ_1:19;
end;

theorem Th15: :: FINSEQ_6:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2, f3 being FinSequence st f1 c= f2 holds
f3 ^ f1 c= f3 ^ f2
proof end;

theorem Th16: :: FINSEQ_6:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for i being Nat holds (f1 ^ f2) | (Seg ((len f1) + i)) = f1 ^ (f2 | (Seg i))
proof end;

theorem Th17: :: FINSEQ_6:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f2, f1 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -| p = f1 ^ (f2 -| p)
proof end;

theorem :: FINSEQ_6:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: FINSEQ_6:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for p being set st f1 ^ f2 just_once_values p holds
p in (rng f1) \+\ (rng f2)
proof end;

theorem :: FINSEQ_6:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence
for p being set st f1 ^ f2 just_once_values p & p in rng f1 holds
f1 just_once_values p
proof end;

theorem Th21: :: FINSEQ_6:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence st not rng f is trivial holds
not f is trivial
proof end;

theorem Th22: :: FINSEQ_6:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being set holds p .. <*p*> = 1
proof end;

theorem Th23: :: FINSEQ_6:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being set holds p1 .. <*p1,p2*> = 1
proof end;

theorem Th24: :: FINSEQ_6:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being set st p1 <> p2 holds
p2 .. <*p1,p2*> = 2
proof end;

theorem Th25: :: FINSEQ_6:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being set holds p1 .. <*p1,p2,p3*> = 1
proof end;

theorem Th26: :: FINSEQ_6:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being set st p1 <> p2 holds
p2 .. <*p1,p2,p3*> = 2
proof end;

theorem Th27: :: FINSEQ_6:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p3, p2 being set st p1 <> p3 & p2 <> p3 holds
p3 .. <*p1,p2,p3*> = 3
proof end;

theorem Th28: :: FINSEQ_6:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being set
for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*>
proof end;

theorem Th29: :: FINSEQ_6:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence holds Rev (Rev f) = f
proof end;

theorem Th30: :: FINSEQ_6:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set st x <> y holds
<*x,y*> -| y = <*x*>
proof end;

theorem Th31: :: FINSEQ_6:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set st x <> y holds
<*x,y,z*> -| y = <*x*>
proof end;

theorem Th32: :: FINSEQ_6:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, z, y being set st x <> z & y <> z holds
<*x,y,z*> -| z = <*x,y*>
proof end;

theorem :: FINSEQ_6:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds <*x,y*> |-- x = <*y*>
proof end;

theorem Th34: :: FINSEQ_6:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set st x <> y holds
<*x,y,z*> |-- y = <*z*>
proof end;

theorem :: FINSEQ_6:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds <*x,y,z*> |-- x = <*y,z*>
proof end;

theorem Th36: :: FINSEQ_6:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being set holds
( <*z*> |-- z = {} & <*z*> -| z = {} )
proof end;

theorem Th37: :: FINSEQ_6:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set st x <> y holds
<*x,y*> |-- y = {}
proof end;

theorem Th38: :: FINSEQ_6:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, z, y being set st x <> z & y <> z holds
<*x,y,z*> |-- z = {}
proof end;

theorem Th39: :: FINSEQ_6:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being FinSequence st x in rng f & y in rng (f -| x) holds
(f -| x) -| y = f -| y
proof end;

theorem Th40: :: FINSEQ_6:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f1, f2 being FinSequence st not x in rng f1 holds
x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1
proof end;

theorem Th41: :: FINSEQ_6:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being FinSequence st f just_once_values x holds
(x .. f) + (x .. (Rev f)) = (len f) + 1
proof end;

theorem Th42: :: FINSEQ_6:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being FinSequence st f just_once_values x holds
Rev (f -| x) = (Rev f) |-- x
proof end;

theorem :: FINSEQ_6:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being FinSequence st f just_once_values x holds
Rev f just_once_values x
proof end;

theorem Th44: :: FINSEQ_6:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f -: p = (f -| p) ^ <*p*>
proof end;

theorem Th45: :: FINSEQ_6:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f :- p = <*p*> ^ (f |-- p)
proof end;

theorem Th46: :: FINSEQ_6:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of D st f <> {} holds
f /. 1 in rng f
proof end;

theorem Th47: :: FINSEQ_6:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of D st f <> {} holds
(f /. 1) .. f = 1
proof end;

theorem Th48: :: FINSEQ_6:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st f <> {} & f /. 1 = p holds
( f -: p = <*p*> & f :- p = f )
proof end;

theorem Th49: :: FINSEQ_6:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1 being Element of D
for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f
proof end;

theorem Th50: :: FINSEQ_6:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D holds <*p1,p2*> /^ 1 = <*p2*>
proof end;

theorem Th51: :: FINSEQ_6:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2, p3 being Element of D holds <*p1,p2,p3*> /^ 1 = <*p2,p3*>
proof end;

theorem Th52: :: FINSEQ_6:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set
for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds
f /. i <> f /. k ) holds
(f /. k) .. f = k
proof end;

theorem Th53: :: FINSEQ_6:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D st p1 <> p2 holds
<*p1,p2*> -: p2 = <*p1,p2*>
proof end;

theorem Th54: :: FINSEQ_6:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p2 holds
<*p1,p2,p3*> -: p2 = <*p1,p2*>
proof end;

theorem Th55: :: FINSEQ_6:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds
<*p1,p2,p3*> -: p3 = <*p1,p2,p3*>
proof end;

theorem :: FINSEQ_6:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D holds
( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )
proof end;

theorem Th57: :: FINSEQ_6:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D st p1 <> p2 holds
<*p1,p2*> :- p2 = <*p2*>
proof end;

theorem Th58: :: FINSEQ_6:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p2 holds
<*p1,p2,p3*> :- p2 = <*p2,p3*>
proof end;

theorem Th59: :: FINSEQ_6:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p3, p2 being Element of D st p1 <> p3 & p2 <> p3 holds
<*p1,p2,p3*> :- p3 = <*p3*>
proof end;

theorem :: FINSEQ_6:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th61: :: FINSEQ_6:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
p .. f = k + (p .. (f /^ k))
proof end;

theorem Th62: :: FINSEQ_6:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
p in rng (f /^ k)
proof end;

theorem Th63: :: FINSEQ_6:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for D being non empty set
for f being FinSequence of D st k < i & i in dom f holds
f /. i in rng (f /^ k)
proof end;

theorem Th64: :: FINSEQ_6:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
(f /^ k) -: p = (f -: p) /^ k
proof end;

theorem Th65: :: FINSEQ_6:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f <> 1 holds
(f /^ 1) -: p = (f -: p) /^ 1
proof end;

theorem Th66: :: FINSEQ_6:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (f :- p)
proof end;

theorem Th67: :: FINSEQ_6:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for D being non empty set
for p being Element of D
for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds
x in rng (f :- p)
proof end;

theorem Th68: :: FINSEQ_6:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds
f /. k in rng (f :- p)
proof end;

theorem Th69: :: FINSEQ_6:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) :- p = (f1 :- p) ^ f2
proof end;

theorem Th70: :: FINSEQ_6:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) :- p = f2 :- p
proof end;

theorem Th71: :: FINSEQ_6:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f1, f2 being FinSequence of D st p in rng f1 holds
(f1 ^ f2) -: p = f1 -: p
proof end;

theorem Th72: :: FINSEQ_6:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f2, f1 being FinSequence of D st p in (rng f2) \ (rng f1) holds
(f1 ^ f2) -: p = f1 ^ (f2 -: p)
proof end;

theorem :: FINSEQ_6:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D holds (f :- p) :- p = f :- p
proof end;

theorem Th74: :: FINSEQ_6:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds
f |-- p2 = (f |-- p1) |-- p2
proof end;

theorem Th75: :: FINSEQ_6:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
rng f = (rng (f -: p)) \/ (rng (f :- p))
proof end;

theorem Th76: :: FINSEQ_6:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in (rng f) \ (rng (f -: p1)) holds
(f :- p1) :- p2 = f :- p2
proof end;

theorem Th77: :: FINSEQ_6:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
p .. (f -: p) = p .. f
proof end;

theorem Th78: :: FINSEQ_6:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for D being non empty set
for f being FinSequence of D holds (f | i) | i = f | i
proof end;

theorem Th79: :: FINSEQ_6:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f -: p) -: p = f -: p
proof end;

theorem Th80: :: FINSEQ_6:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D
for f being FinSequence of D st p1 in rng f & p2 in rng (f -: p1) holds
(f -: p1) -: p2 = f -: p2
proof end;

theorem Th81: :: FINSEQ_6:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(f -: p) ^ ((f :- p) /^ 1) = f
proof end;

theorem Th82: :: FINSEQ_6:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f1, f2 being FinSequence of D st f1 <> {} holds
(f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2
proof end;

theorem Th83: :: FINSEQ_6:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p2 being Element of D
for f being FinSequence of D st p2 in rng f & p2 .. f <> 1 holds
p2 in rng (f /^ 1)
proof end;

theorem Th84: :: FINSEQ_6:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D holds p .. (f :- p) = 1
proof end;

Lm3: for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > i holds
i + (p .. (f /^ i)) = p .. f
proof end;

theorem :: FINSEQ_6:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th86: :: FINSEQ_6:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set holds (<*> D) /^ k = <*> D
proof end;

theorem Th87: :: FINSEQ_6:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat
for D being non empty set
for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k
proof end;

theorem Th88: :: FINSEQ_6:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
(f /^ k) :- p = f :- p
proof end;

theorem Th89: :: FINSEQ_6:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f <> 1 holds
(f /^ 1) :- p = f :- p
proof end;

theorem Th90: :: FINSEQ_6:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat
for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i
proof end;

theorem Th91: :: FINSEQ_6:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat
for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f | k) = (Rev f) /^ i
proof end;

theorem Th92: :: FINSEQ_6:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f |-- p) = (Rev f) -| p
proof end;

theorem Th93: :: FINSEQ_6:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f :- p) = (Rev f) -: p
proof end;

theorem Th94: :: FINSEQ_6:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f -: p) = (Rev f) :- p
proof end;

definition
let D be non empty set ;
let IT be FinSequence of D;
attr IT is circular means :Def1: :: FINSEQ_6:def 1
IT /. 1 = IT /. (len IT);
end;

:: deftheorem Def1 defines circular FINSEQ_6:def 1 :
for D being non empty set
for IT being FinSequence of D holds
( IT is circular iff IT /. 1 = IT /. (len IT) );

definition
let D be non empty set ;
let f be FinSequence of D;
let p be Element of D;
func Rotate f,p -> FinSequence of D equals :Def2: :: FINSEQ_6:def 2
(f :- p) ^ ((f -: p) /^ 1) if p in rng f
otherwise f;
correctness
coherence
( ( p in rng f implies (f :- p) ^ ((f -: p) /^ 1) is FinSequence of D ) & ( not p in rng f implies f is FinSequence of D ) )
;
consistency
for b1 being FinSequence of D holds verum
;
;
end;

:: deftheorem Def2 defines Rotate FINSEQ_6:def 2 :
for D being non empty set
for f being FinSequence of D
for p being Element of D holds
( ( p in rng f implies Rotate f,p = (f :- p) ^ ((f -: p) /^ 1) ) & ( not p in rng f implies Rotate f,p = f ) );

registration
let D be non empty set ;
let f be non empty FinSequence of D;
let p be Element of D;
cluster Rotate f,p -> non empty ;
coherence
not Rotate f,p is empty
proof end;
end;

registration
let D be non empty set ;
cluster non empty trivial circular FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is circular & not b1 is empty & b1 is trivial )
proof end;
cluster non empty non trivial circular FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is circular & not b1 is empty & not b1 is trivial )
proof end;
end;

theorem Th95: :: FINSEQ_6:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of D holds Rotate f,(f /. 1) = f
proof end;

registration
let D be non empty set ;
let p be Element of D;
let f be non empty circular FinSequence of D;
cluster Rotate f,p -> non empty circular ;
coherence
Rotate f,p is circular
proof end;
end;

theorem :: FINSEQ_6:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is circular & p in rng f holds
rng (Rotate f,p) = rng f
proof end;

theorem Th97: :: FINSEQ_6:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
p in rng (Rotate f,p)
proof end;

theorem Th98: :: FINSEQ_6:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
(Rotate f,p) /. 1 = p
proof end;

theorem Th99: :: FINSEQ_6:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D holds Rotate (Rotate f,p),p = Rotate f,p
proof end;

theorem :: FINSEQ_6:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D holds Rotate <*p*>,p = <*p*>
proof end;

theorem Th101: :: FINSEQ_6:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D holds Rotate <*p1,p2*>,p1 = <*p1,p2*>
proof end;

theorem :: FINSEQ_6:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2 being Element of D holds Rotate <*p1,p2*>,p2 = <*p2,p2*>
proof end;

theorem Th103: :: FINSEQ_6:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2, p3 being Element of D holds Rotate <*p1,p2,p3*>,p1 = <*p1,p2,p3*>
proof end;

theorem :: FINSEQ_6:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p2 holds
Rotate <*p1,p2,p3*>,p2 = <*p2,p3,p2*>
proof end;

theorem :: FINSEQ_6:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p2, p3, p1 being Element of D st p2 <> p3 holds
Rotate <*p1,p2,p3*>,p3 = <*p3,p2,p3*>
proof end;

theorem :: FINSEQ_6:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f
proof end;

theorem Th107: :: FINSEQ_6:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate f,p)
proof end;

theorem Th108: :: FINSEQ_6:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p2, p1 being Element of D
for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds
Rotate (Rotate f,p1),p2 = Rotate f,p2
proof end;

theorem Th109: :: FINSEQ_6:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p2, p1 being Element of D
for f being FinSequence of D st p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds
Rotate (Rotate f,p1),p2 = Rotate f,p2
proof end;

theorem Th110: :: FINSEQ_6:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p2, p1 being Element of D
for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 holds
Rotate (Rotate f,p1),p2 = Rotate f,p2
proof end;

theorem :: FINSEQ_6:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p2, p1 being Element of D
for f being FinSequence of D st f is circular & f just_once_values p2 holds
Rotate (Rotate f,p1),p2 = Rotate f,p2
proof end;

theorem :: FINSEQ_6:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for p being Element of D
for f being FinSequence of D st f is circular & f just_once_values p holds
Rev (Rotate f,p) = Rotate (Rev f),p
proof end;