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

theorem Th1: :: FINSEQ_7:1  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
for i, j being Nat st 1 <= i & j <= len f & i < j holds
f = ((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)
proof end;

theorem :: FINSEQ_7:2  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 f, g, h being FinSequence st len g = len h & len g < i & i <= len (g ^ f) holds
(g ^ f) . i = (h ^ f) . i
proof end;

theorem :: FINSEQ_7:3  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 f, g being FinSequence st 1 <= i & i <= len f holds
f . i = (g ^ f) . ((len g) + i)
proof end;

theorem :: FINSEQ_7:4  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
for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i)
proof end;

Lm1: for j, i being Nat holds (j -' i) -' 1 = (j -' 1) -' i
proof end;

notation
let D be non empty set ;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
synonym Replace f,i,p for D +* f,i;
end;

definition
let D be non empty set ;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
:: original: Replace
redefine func Replace f,i,p -> FinSequence of D equals :Def1: :: FINSEQ_7:def 1
((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) if ( 1 <= i & i <= len f )
otherwise f;
compatibility
for b1 being FinSequence of D holds
( ( 1 <= i & i <= len f implies ( b1 = Replace i,p, iff b1 = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) ) & ( ( not 1 <= i or not i <= len f ) implies ( b1 = Replace i,p, iff b1 = f ) ) )
proof end;
correctness
coherence
Replace i,p, is FinSequence of D
;
consistency
for b1 being FinSequence of D holds verum
;
proof end;
end;

:: deftheorem Def1 defines Replace FINSEQ_7:def 1 :
for D being non empty set
for f being FinSequence of D
for i being Nat
for p being Element of D holds
( ( 1 <= i & i <= len f implies Replace f,i,p = ((f | (i -' 1)) ^ <*p*>) ^ (f /^ i) ) & ( ( not 1 <= i or not i <= len f ) implies Replace f,i,p = f ) );

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

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

theorem Th7: :: FINSEQ_7:7  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
for p being Element of D
for i being Nat holds len (Replace f,i,p) = len f
proof end;

theorem :: FINSEQ_7:8  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
for p being Element of D
for i being Nat holds rng (Replace f,i,p) c= (rng f) \/ {p}
proof end;

theorem :: FINSEQ_7:9  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
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace f,i,p)
proof end;

Lm2: for D being non empty set
for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace f,i,p) . i = p
proof end;

theorem :: FINSEQ_7:10  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
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
(Replace f,i,p) /. i = p
proof end;

theorem :: FINSEQ_7:11  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
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
for k being Nat st 0 < k & k <= (len f) - i holds
(Replace f,i,p) . (i + k) = (f /^ i) . k
proof end;

theorem Th12: :: FINSEQ_7:12  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
for p being Element of D
for k, i being Nat st 1 <= k & k <= len f & k <> i holds
(Replace f,i,p) /. k = f /. k
proof end;

theorem Th13: :: FINSEQ_7:13  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
for q, p being Element of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Replace (Replace f,j,q),i,p = ((((f | (i -' 1)) ^ <*p*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*q*>) ^ (f /^ j)
proof end;

theorem :: FINSEQ_7:14  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, q being Element of D holds Replace <*p*>,1,q = <*q*>
proof end;

theorem Th15: :: FINSEQ_7:15  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, q being Element of D holds Replace <*p1,p2*>,1,q = <*q,p2*>
proof end;

theorem Th16: :: FINSEQ_7:16  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, q being Element of D holds Replace <*p1,p2*>,2,q = <*p1,q*>
proof end;

theorem Th17: :: FINSEQ_7:17  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, q being Element of D holds Replace <*p1,p2,p3*>,1,q = <*q,p2,p3*>
proof end;

theorem Th18: :: FINSEQ_7:18  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, q being Element of D holds Replace <*p1,p2,p3*>,2,q = <*p1,q,p3*>
proof end;

theorem Th19: :: FINSEQ_7:19  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, q being Element of D holds Replace <*p1,p2,p3*>,3,q = <*p1,p2,q*>
proof end;

definition
let D be non empty set ;
let f be FinSequence of D;
let i, j be Nat;
func Swap f,i,j -> FinSequence of D equals :Def2: :: FINSEQ_7:def 2
Replace (Replace f,i,(f /. j)),j,(f /. i) if ( 1 <= i & i <= len f & 1 <= j & j <= len f )
otherwise f;
correctness
coherence
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Replace (Replace f,i,(f /. j)),j,(f /. i) is FinSequence of D ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies f is FinSequence of D ) )
;
consistency
for b1 being FinSequence of D holds verum
;
;
end;

:: deftheorem Def2 defines Swap FINSEQ_7:def 2 :
for D being non empty set
for f being FinSequence of D
for i, j being Nat holds
( ( 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap f,i,j = Replace (Replace f,i,(f /. j)),j,(f /. i) ) & ( ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) implies Swap f,i,j = f ) );

theorem Th20: :: FINSEQ_7:20  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
for i, j being Nat holds len (Swap f,i,j) = len f
proof end;

Lm3: for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )
proof end;

theorem Th21: :: FINSEQ_7:21  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
for i being Nat holds Swap f,i,i = f
proof end;

theorem :: FINSEQ_7:22  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
for i, j being Nat holds Swap (Swap f,i,j),j,i = f
proof end;

theorem Th23: :: FINSEQ_7:23  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
for i, j being Nat holds Swap f,i,j = Swap f,j,i
proof end;

theorem :: FINSEQ_7:24  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
for i, j being Nat holds rng (Swap f,i,j) = rng f
proof end;

theorem :: FINSEQ_7:25  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 Swap <*p1,p2*>,1,2 = <*p2,p1*>
proof end;

theorem :: FINSEQ_7:26  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 Swap <*p1,p2,p3*>,1,2 = <*p2,p1,p3*>
proof end;

theorem :: FINSEQ_7:27  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 Swap <*p1,p2,p3*>,1,3 = <*p3,p2,p1*>
proof end;

theorem :: FINSEQ_7:28  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 Swap <*p1,p2,p3*>,2,3 = <*p1,p3,p2*>
proof end;

theorem Th29: :: FINSEQ_7:29  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
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap f,i,j = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
proof end;

theorem :: FINSEQ_7:30  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
for i being Nat st 1 < i & i <= len f holds
Swap f,1,i = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)
proof end;

theorem :: FINSEQ_7:31  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
for i being Nat st 1 <= i & i < len f holds
Swap f,i,(len f) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>
proof end;

Lm4: for D being non empty set
for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k holds
(Swap f,i,j) . k = f . k
proof end;

theorem Th32: :: FINSEQ_7:32  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
for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap f,i,j) /. k = f /. k
proof end;

theorem Th33: :: FINSEQ_7:33  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
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap f,i,j) /. i = f /. j & (Swap f,i,j) /. j = f /. i )
proof end;

theorem Th34: :: FINSEQ_7:34  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
for p being Element of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
Replace (Swap f,i,j),i,p = Swap (Replace f,j,p),i,j
proof end;

theorem Th35: :: FINSEQ_7:35  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
for p being Element of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap (Replace f,k,p),i,j = Replace (Swap f,i,j),k,p
proof end;

theorem :: FINSEQ_7:36  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
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap (Swap f,i,j),j,k = Swap (Swap f,i,k),i,j
proof end;

theorem :: FINSEQ_7:37  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
for i, k, j, l being Nat st i <> k & j <> k & l <> i & l <> j & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f & 1 <= l & l <= len f holds
Swap (Swap f,i,j),k,l = Swap (Swap f,k,l),i,j
proof end;