:: On Replace Function and Swap Function for Finite Sequences
:: by Hiroshi Yamazaki , Yoshinori Fujisawa and Yatsuka Nakamura
::
:: Received August 28, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, SUBSET_1, NAT_1, XXREAL_0, ARYTM_3,
RELAT_1, ARYTM_1, ORDINAL4, FUNCT_1, RFINSEQ, PARTFUN1, CARD_1, AFINSQ_1,
FUNCT_4, TARSKI, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, RFINSEQ, FUNCT_7,
XXREAL_0;
constructors PARTFUN1, FUNCT_4, XXREAL_0, REAL_1, NAT_1, INT_1, FINSEQ_4,
RFINSEQ, NAT_D, FUNCT_7, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FUNCT_7,
ORDINAL1, NAT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions FINSEQ_1;
equalities FINSEQ_1;
expansions FINSEQ_1;
theorems NAT_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, FINSEQ_6, RFINSEQ, INT_1,
GENEALG1, FUNCT_7, XREAL_1, XXREAL_0, ORDINAL1, NAT_2, PARTFUN1, NAT_D,
XREAL_0;
begin :: Some Basic Theorems
reserve D for non empty set,
f for FinSequence of D,
p, p1, p2, p3, q for Element of D,
i, j, k, l, n for Nat;
theorem
1 <= i & j <= len f & i < j implies f = (f|(i-'1))^<*f.i*>^((f/^i)|(j
-'i-'1))^<*f.j*>^(f/^j)
proof
assume that
A1: 1 <= i and
A2: j <= len f and
A3: i < j;
A4: i <= len f by A2,A3,XXREAL_0:2;
1 <= j by A1,A3,XXREAL_0:2;
then
A5: j in dom f by A2,FINSEQ_3:25;
set I = j-'i-'1;
i -'i < j -'i by A3,NAT_D:57;
then
A6: I + 1 = j -'i by NAT_1:14,XREAL_1:235;
j -'i <= len f -'i by A2,NAT_D:42;
then
A7: I+1 <= len (f/^i) by A6,RFINSEQ:29;
reconsider i,j as Element of NAT by ORDINAL1:def 12;
A8: i < len (f|j) by A2,A3,FINSEQ_1:59;
1 <= I+1 by NAT_1:14;
then
A9: I+1 in dom (f/^i) by A7,FINSEQ_3:25;
(I+1)+i = j by A3,A6,XREAL_1:235;
then
A10: (f/^i)/.(I+1) = f/.j by A9,FINSEQ_5:27;
A11: f/^i = ((f|j)^(f/^j))/^i by RFINSEQ:8
.= ((f|j)/^i)^(f/^j) by A8,GENEALG1:1
.= ((f/^i)|(I+1))^(f/^j) by A6,FINSEQ_5:80
.= ((f/^i)|I)^<*(f/^i)/.(I+1)*>^(f/^j) by A7,FINSEQ_5:82
.= ((f/^i)|I)^<*f.j*>^(f/^j) by A5,A10,PARTFUN1:def 6;
f = (f|(i-'1))^<*f.i*>^(f/^i) by A1,A4,FINSEQ_5:84
.= (f|(i-'1))^<*f.i*>^(((f/^i)|I)^(<*f.j*>^(f/^j))) by A11,FINSEQ_1:32
.= (f|(i-'1))^<*f.i*>^((f/^i)|I)^(<*f.j*>^(f/^j)) by FINSEQ_1:32
.= (f|(i-'1))^<*f.i*>^((f/^i)|I)^<*f.j*>^(f/^j) by FINSEQ_1:32;
hence thesis;
end;
theorem
for f,g,h being FinSequence holds len g = len h & len g < i & i <= len
(g^f) implies (g^f).i = (h^f).i
proof
let f,g,h be FinSequence;
assume that
A1: len g = len h and
A2: len g < i and
A3: i <= len (g^f);
i <= len g + len f by A3,FINSEQ_1:22;
then
A4: i - len g <= len g + len f - len g by XREAL_1:9;
set k = i - len g;
A5: len g - len g < i - len g by A2,XREAL_1:9;
then reconsider k as Element of NAT by INT_1:3;
0 + 1 <= i - len g by A5,INT_1:7;
then
A6: k in dom f by A4,FINSEQ_3:25;
(g^f).i = (g^f).(k + len g) .= f.k by A6,FINSEQ_1:def 7
.= (h^f).(len h + k) by A6,FINSEQ_1:def 7;
hence thesis by A1;
end;
theorem
for f,g being FinSequence st 1 <= i & i <= len f holds
f.i = (g^f).(len g + i)
proof
let f,g be FinSequence;
assume 1 <= i & i <= len f;
then i in dom f by FINSEQ_3:25;
hence thesis by FINSEQ_1:def 7;
end;
theorem
i in dom(f/^n) implies (f/^n).i = f.(n+i) by FINSEQ_5:27;
Lm1: j -'i -'1 = j -'1 -'i
proof
j -'i -'1 = j -'(i+1) by NAT_2:30;
hence thesis by NAT_2:30;
end;
begin :: Definition of Replace Function and its properties
notation
let f be FinSequence;
let i be Nat;
let p be object;
synonym Replace(f, i, p) for f +* (i, p);
end;
definition
let D be non empty set;
let f be FinSequence of D;
let i be Nat;
let p be Element of D;
redefine func Replace(f, i, p) -> FinSequence of D equals :: redefines Replace (FINSEQ_7, synonym) → +* (FUNCT_7, definition)
:Def1:
(f|(i-'1))^<*p*>^(f/^i) if 1 <= i & i <= len f otherwise f;
compatibility
proof
A1: not (1 <= i & i <= len f) implies f +* (i, p) = f
proof
assume not (1 <= i & i <= len f);
then not i in dom f by FINSEQ_3:25;
hence thesis by FUNCT_7:def 3;
end;
1 <= i & i <= len f implies f +* (i, p) = (f|(i-'1))^<*p*>^(f/^i)
proof
assume 1 <= i & i <= len f;
then i in dom f by FINSEQ_3:25;
hence thesis by FUNCT_7:98;
end;
hence thesis by A1;
end;
correctness
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
f +* (i, p) is FinSequence of D;
hence thesis;
end;
end;
theorem
len Replace(f, i, p) = len f by FUNCT_7:97;
theorem
for f being FinSequence, i be Nat, p be set
holds rng Replace(f, i, p) c= rng f \/ {p} by FUNCT_7:100;
theorem
1 <= i & i <= len f implies p in rng Replace(f, i, p)
proof
assume 1 <= i & i <= len f;
then i in dom f by FINSEQ_3:25;
hence thesis by FUNCT_7:102;
end;
Lm2: 1 <= i & i <= len f implies Replace(f, i, p).i = p
proof
assume 1 <= i & i <= len f;
then i in dom f by FINSEQ_3:25;
hence thesis by FUNCT_7:31;
end;
theorem
1 <= i & i <= len f implies Replace(f, i, p)/.i = p
proof
assume 1 <= i & i <= len f;
then i in dom f by FINSEQ_3:25;
hence thesis by FUNCT_7:36;
end;
theorem
1 <= i & i <= len f implies for k st 0 < k & k <= len f - i holds
Replace(f, i, p).(i + k) = (f/^i).k
proof
assume that
A1: 1 <= i and
A2: i <= len f;
i - 1 < i by XREAL_1:146;
then
A3: i -' 1 < i by A1,XREAL_1:233;
A4: len ((f|(i-'1))^<*p*>) = len (f|(i-'1)) + len <*p*> by FINSEQ_1:22
.= (i -' 1) + len <*p*> by A2,A3,FINSEQ_1:59,XXREAL_0:2
.= i -' 1 + 1 by FINSEQ_1:39
.= i by A1,XREAL_1:235;
let k;
assume that
A5: 0 < k and
A6: k <= len f - i;
A7: 0 + 1 <= k by A5,INT_1:7;
len f = len Replace(f, i, p) by FUNCT_7:97
.= len ((f|(i-'1))^<*p*>^(f/^i)) by A1,A2,Def1
.= i + len (f/^i) by A4,FINSEQ_1:22;
then
A8: k in dom (f/^i) by A6,A7,FINSEQ_3:25;
Replace(f, i, p).(i + k) = ((f|(i-'1))^<*p*>^(f/^i)).(len ((f|(i-'1))^
<*p*>) + k) by A1,A2,A4,Def1;
hence thesis by A8,FINSEQ_1:def 7;
end;
theorem Th10:
1 <= k & k <= len f & k <> i implies Replace(f, i, p)/.k = f/.k
proof
assume
A1: 1 <= k & k <= len f & k <> i;
reconsider i,k as Element of NAT by ORDINAL1:def 12;
k <> i & k in dom f by A1,FINSEQ_3:25;
hence thesis by FUNCT_7:37;
end;
theorem Th11:
1 <= i & i < j & j <= len f implies Replace(Replace(f, j, q), i, p) =
(f|(i-'1))^<*p*>^(f/^i)|(j-'i-'1)^<*q*>^(f/^j)
proof
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f;
set fp = f|(j-'1);
A4: j -'1 <= j by NAT_D:35;
1 + i <= j by A2,INT_1:7;
then i <= j -' 1 by NAT_D:55;
then
A5: i <= len fp by A3,A4,FINSEQ_1:59,XXREAL_0:2;
set Q = f/^j;
set F = Replace(f,j,q);
A6: 1 <= j by A1,A2,XXREAL_0:2;
set fj = <*q*>;
set P = fp^fj;
A7: len P = len fp + len fj by FINSEQ_1:22
.= len fp + 1 by FINSEQ_1:39
.= j -'1 + 1 by A3,A4,FINSEQ_1:59,XXREAL_0:2
.= j by A1,A2,XREAL_1:235,XXREAL_0:2;
A8: i -'1 < j -'1 by A1,A2,NAT_D:56;
then
A9: i-'1 <= len fp by A3,A4,FINSEQ_1:59,XXREAL_0:2;
i <= len f by A2,A3,XXREAL_0:2;
then i <= len F by FUNCT_7:97;
then Replace(F,i,p) = (F|(i-'1))^<*p*>^(F/^i) by A1,Def1
.= (F|(i-'1))^<*p*>^((P^Q)/^i) by A3,A6,Def1
.= (F|(i-'1))^<*p*>^((P/^i)^Q) by A2,A7,GENEALG1:1
.= (F|(i-'1))^<*p*>^(((fp/^i)^fj)^Q) by A5,GENEALG1:1
.= (F|(i-'1))^<*p*>^((((f/^i)|((j-'1)-'i))^fj)^Q) by FINSEQ_5:80
.= (F|(i-'1))^<*p*>^(((f/^i)|((j-'1)-'i))^fj)^Q by FINSEQ_1:32
.= (F|(i-'1))^<*p*>^((f/^i)|((j-'1)-'i))^fj^Q by FINSEQ_1:32
.= ((P^Q)|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A3,A6,Def1
.= (P|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A2,A7,FINSEQ_5:22,NAT_D:44
.= (fp|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A9,FINSEQ_5:22
.= (f|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A8,FINSEQ_5:77
.= (f|(i-'1))^<*p*>^(f/^i)|(j-'i-'1)^<*q*>^Q by Lm1;
hence thesis;
end;
theorem
Replace(<*p*>, 1, q) = <*q*>
proof
A1: 1 - 1 = 0;
set g = <*>D;
reconsider P = <*p*>^g as FinSequence of D;
A2: (<*p*>^g)/^1 = g by FINSEQ_6:45;
1 <= len <*p*> by FINSEQ_1:39;
hence Replace(<*p*>, 1, q) = (<*p*>|(1-'1))^<*q*>^(<*p*>/^1) by Def1
.= (<*p*>|0)^<*q*>^(<*p*>/^1) by A1,XREAL_0:def 2
.= <*q*>^(<*p*>/^1) by FINSEQ_1:34
.= <*q*>^(P/^1) by FINSEQ_1:34
.= <*q*> by A2,FINSEQ_1:34;
end;
theorem Th13:
Replace(<*p1, p2*>, 1, q) = <*q, p2*>
proof
set f = <*p1,p2*>;
A1: len f = 2 by FINSEQ_1:44;
1 + 1 = len f by FINSEQ_1:44;
then
A3: f/^1 = <*f.2*> by FINSEQ_5:30;
Replace(f,1,q) = (f|(1-'1))^<*q*>^(f/^1) by A1,Def1
.= (f|0)^<*q*>^(f/^1) by XREAL_1:232
.= {}^<*q*>^<*p2*> by A3
.= <*q*>^<*p2*> by FINSEQ_1:34;
hence thesis;
end;
theorem Th14:
Replace(<*p1, p2*>, 2, q) = <*p1, q*>
proof
set f = <*p1,p2*>;
A1: 2 -'1 = 1 + 1 -'1 .= 1 by NAT_D:34;
2 <= len f by FINSEQ_1:44;
then Replace(f,2,q) = (f|(2-'1))^<*q*>^(f/^2) by Def1
.= (f|1)^<*q*>^(f/^len f) by A1,FINSEQ_1:44
.= (f|1)^<*q*>^{} by RFINSEQ:27
.= <*f.1*>^<*q*>^{} by FINSEQ_5:20
.= <*f.1*>^<*q*> by FINSEQ_1:34
.= <*p1*>^<*q*>;
hence thesis;
end;
theorem Th15:
Replace(<*p1, p2, p3*>, 1, q) = <*q, p2, p3*>
proof
set f = <*p1,p2,p3*>;
len f = 3 by FINSEQ_1:45;
then Replace(f,1,q) = (f|(1-'1))^<*q*>^(f/^1) by Def1
.= (f|0)^<*q*>^(f/^1) by XREAL_1:232
.= <*q*>^(f/^1) by FINSEQ_1:34
.= <*q*>^<*p2,p3*> by FINSEQ_6:47
.= <*q*>^<*p2*>^<*p3*> by FINSEQ_1:32;
hence thesis;
end;
theorem Th16:
Replace(<*p1, p2, p3*>, 2, q) = <*p1, q, p3*>
proof
set f = <*p1,p2,p3*>;
A1: 2 -'1 = 1 + 1 -'1 .= 1 by NAT_D:34;
A2: len f = 2 + 1 by FINSEQ_1:45;
len f = 3 by FINSEQ_1:45; then
Replace(f,2,q) = (f|(2-'1))^<*q*>^(f/^2) by Def1
.= (f|1)^<*q*>^<*f.3*> by A1,A2,FINSEQ_5:30
.= (f|1)^<*q*>^<*p3*>
.= <*f.1*>^<*q*>^<*p3*> by FINSEQ_5:20
.= <*p1*>^<*q*>^<*p3*>;
hence thesis;
end;
theorem Th17:
Replace(<*p1, p2, p3*>, 3, q) = <*p1, p2, q*>
proof
set f = <*p1,p2,p3*>;
A1: 3 -'1 = 2 + 1 -'1 .= 2 by NAT_D:34;
A2: len f = 3 by FINSEQ_1:45;
then
A3: 1 in dom f by FINSEQ_3:25;
A4: 2 in dom f by A2,FINSEQ_3:25;
3 <= len f by FINSEQ_1:45;
then Replace(f,3,q) = (f|(3-'1))^<*q*>^(f/^3) by Def1
.= (f|2)^<*q*>^(f/^len f) by A1,FINSEQ_1:45
.= (f|2)^<*q*>^{} by RFINSEQ:27
.= (f|2)^<*q*> by FINSEQ_1:34
.= <*f/.1,f/.2*>^<*q*> by A2,FINSEQ_5:81
.= <*f.1*>^<*f/.2*>^<*q*> by A3,PARTFUN1:def 6
.= <*f.1*>^<*f.2*>^<*q*> by A4,PARTFUN1:def 6
.= <*p1*>^<*f.2*>^<*q*>
.= <*p1*>^<*p2*>^<*q*>;
hence thesis;
end;
begin :: Definition of Swap Function and its properties
registration
let f be FinSequence;
let i, j be Nat;
cluster Swap(f, i, j) -> FinSequence-like;
correctness
proof
dom Swap(f, i, j) = dom f by FUNCT_7:99;
hence ex n being Nat st dom Swap(f, i, j) = Seg n by FINSEQ_1:def 2;
end;
end;
definition
let D be non empty set;
let f be FinSequence of D;
let i, j be Nat;
redefine func Swap(f, i, j) -> FinSequence of D equals :: redefines Swap (FUNCT_7, definition)
:Def2:
Replace(
Replace(f, i, f/.j), j, f/.i) if 1 <= i & i <= len f & 1 <= j & j <= len f
otherwise f;
coherence
proof
rng Swap(f,i,j) = rng f by FUNCT_7:103;
hence rng Swap(f, i, j) c= D by FINSEQ_1:def 4;
end;
compatibility
proof
let IT be FinSequence of D;
thus 1 <= i & i <= len f & 1 <= j & j <= len f implies (IT = Swap(f, i, j)
iff IT = Replace(Replace(f, i, f/.j), j, f/.i))
proof
assume that
A1: 1 <= i & i <= len f and
A2: 1 <= j & j <= len f;
A3: j in dom f by A2,FINSEQ_3:25;
then
A4: f/.j = f.j by PARTFUN1:def 6;
A5: i in dom f by A1,FINSEQ_3:25;
then f/.i = f.i by PARTFUN1:def 6;
hence thesis by A5,A3,A4,FUNCT_7:def 12;
end;
assume not(1 <= i & i <= len f & 1 <= j & j <= len f);
then not(i in dom f & j in dom f) by FINSEQ_3:25;
hence thesis by FUNCT_7:def 12;
end;
correctness;
end;
theorem Th18:
len Swap(f, i, j) = len f
proof
dom Swap(f, i, j) = dom f by FUNCT_7:99;
hence thesis by FINSEQ_3:29;
end;
Lm3: 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap(f, i, j).i = f.j &
Swap(f, i, j).j = f.i
proof
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f;
A5: i in dom f by A1,A2,FINSEQ_3:25;
set F = Replace (f,i,f/.j);
A6: i <= len F by A2,FUNCT_7:97;
A7: j <= len F by A4,FUNCT_7:97;
A8: j in dom f by A3,A4,FINSEQ_3:25;
per cases;
suppose
A9: i = j;
Swap(f, i, j).i = Replace(F, j, f/.i).i by A1,A2,A3,A4,Def2
.= f/.i by A1,A6,A9,Lm2
.= f.i by A5,PARTFUN1:def 6;
hence thesis by A9;
end;
suppose
A10: i <> j;
A11: Swap(f, i, j).j = Replace(F, j, f/.i).j by A1,A2,A3,A4,Def2
.= f/.i by A3,A7,Lm2;
Swap(f, i, j).i = Replace(F, j, f/.i).i by A1,A2,A3,A4,Def2
.= F.i by A10,FUNCT_7:32
.= f/.j by A1,A2,Lm2;
hence thesis by A5,A8,A11,PARTFUN1:def 6;
end;
end;
theorem Th19:
Swap(f, i, i) = f
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
1 <= i & i <= len f;
then Swap(f, i, i) = Replace(Replace(f, i, f/.i), i, f/.i) by Def2
.= Replace(f, i, f/.i) by FUNCT_7:38;
hence thesis by FUNCT_7:38;
end;
suppose
not (1 <= i & i <= len f);
hence thesis by Def2;
end;
end;
theorem
Swap(Swap(f,i,j),j,i) = f
proof
per cases;
suppose
A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
A2: for k be Nat st 1 <= k & k <= len f holds f.k = Swap(Swap(f,i,j),j,i). k
proof
A3: i <= len Swap(f,i,j) by A1,Th18;
A4: j <= len Swap(f,i,j) by A1,Th18;
let k be Nat;
assume that
A5: 1 <= k and
A6: k <= len f;
A7: k <= len Swap(f,i,j) by A6,Th18;
now
per cases;
suppose
i = k;
then Swap(Swap(f,i,j),j,i).k = Swap(f,k,j).j by A1,A7,A4,Lm3;
hence thesis by A1,A5,A6,Lm3;
end;
suppose
A8: i <> k;
now
per cases;
suppose
j = k;
then Swap(Swap(f,i,j),j,i).k = Swap(f,i,k).i by A1,A7,A3,Lm3;
hence thesis by A1,A5,A6,Lm3;
end;
suppose
A9: j <> k;
set S = Swap(f,i,j);
Swap(S,j,i).k = Replace(Replace(S,j,S/.i),i,S/.j).k by A1,A4,A3
,Def2
.= Replace(S,j,S/.i).k by A8,FUNCT_7:32
.= S.k by A9,FUNCT_7:32
.= Replace(Replace(f,i,f/.j),j,f/.i).k by A1,Def2
.= Replace(f,i,f/.j).k by A9,FUNCT_7:32;
hence thesis by A8,FUNCT_7:32;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
len Swap(Swap(f,i,j),j,i) = len Swap(f,i,j) by Th18
.= len f by Th18;
hence thesis by A2;
end;
suppose
A10: not (1 <= i & i <= len f & 1 <= j & j <= len f);
then Swap(Swap(f,i,j),j,i) = Swap(f,j,i) by Def2;
hence thesis by A10,Def2;
end;
end;
theorem Th21:
Swap(f, i, j) = Swap(f, j, i)
proof
per cases;
suppose
A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
set FJ = Replace(f,j,f/.i);
set FI = Replace(f,i,f/.j);
A2: for k be Nat st 1 <= k & k <= len Swap(f,i,j) holds Swap(f,i,j).k =
Swap(f,j,i).k
proof
A3: len Swap(f,i,j) = len f by Th18
.= len FJ by FUNCT_7:97;
A4: len Swap(f,i,j) = len f by Th18
.= len FI by FUNCT_7:97;
let k be Nat;
assume that
A5: 1 <= k and
A6: k <= len Swap(f,i,j);
A7: k <= len f by A6,Th18;
now
per cases;
suppose
A8: i = k;
now
per cases;
suppose
A9: j = k;
then Swap(f,i,k).k = Replace(FI,k,f/.i).k by A1,Def2
.= f/.i by A5,A6,A4,Lm2
.= Replace(FJ,k,f/.i).k by A5,A6,A3,Lm2
.= Swap(f,k,i).k by A1,A8,A9,Def2;
hence thesis by A9;
end;
suppose
A10: j <> k;
Swap(f,i,j).k = Replace(FI,j,f/.i).k by A1,Def2
.= Replace(f,k,f/.j).k by A8,A10,FUNCT_7:32
.= f/.j by A5,A7,Lm2
.= Replace(FJ,k,f/.j).k by A5,A6,A3,Lm2;
hence thesis by A1,A8,Def2;
end;
end;
hence thesis;
end;
suppose
A11: i <> k;
now
per cases;
suppose
A12: j = k;
then Swap(f,i,j).k = Replace(FI,k,f/.i).k by A1,Def2
.= f/.i by A5,A6,A4,Lm2
.= FJ.k by A5,A7,A12,Lm2
.= Replace(FJ,i,f/.j).k by A11,FUNCT_7:32;
hence thesis by A1,Def2;
end;
suppose
A13: j <> k;
Swap(f,i,j).k = Replace(FI,j,f/.i).k by A1,Def2
.= FI.k by A13,FUNCT_7:32
.= f.k by A11,FUNCT_7:32
.= Replace(f,j,f/.i).k by A13,FUNCT_7:32
.= Replace(FJ,i,f/.j).k by A11,FUNCT_7:32;
hence thesis by A1,Def2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
len Swap(f,i,j) = len f by Th18
.= len Swap(f,j,i) by Th18;
hence thesis by A2;
end;
suppose
A14: not (1 <= i & i <= len f & 1 <= j & j <= len f);
then Swap(f, i, j) = f by Def2;
hence thesis by A14,Def2;
end;
end;
theorem
rng Swap(f,i,j) = rng f by FUNCT_7:103;
theorem
Swap(<*p1, p2*>, 1, 2) = <*p2, p1*>
proof
set f = <*p1,p2*>;
A1: len f = 2 by FINSEQ_1:44;
then 1 in dom f by FINSEQ_3:25;
then
A2: f/.1 = f.1 by PARTFUN1:def 6
.= p1;
2 in dom f by A1,FINSEQ_3:25;
then
A3: f/.2 = f.2 by PARTFUN1:def 6
.= p2;
Swap(f,1,2) = Replace(Replace(f,1,f/.2),2,f/.1) by A1,Def2
.= Replace(<*p2,p2*>,2,f/.1) by A3,Th13;
hence thesis by A2,Th14;
end;
theorem
Swap(<*p1, p2, p3*>, 1, 2) = <*p2, p1, p3*>
proof
set f = <*p1,p2,p3*>;
A1: len f = 3 by FINSEQ_1:45;
then 1 in dom f by FINSEQ_3:25;
then
A2: f/.1 = f.1 by PARTFUN1:def 6
.= p1;
2 in dom f by A1,FINSEQ_3:25;
then
A3: f/.2 = f.2 by PARTFUN1:def 6
.= p2;
Swap(f,1,2) = Replace(Replace(f,1,f/.2),2,f/.1) by A1,Def2
.= Replace(<*p2,p2,p3*>,2,f/.1) by A3,Th15;
hence thesis by A2,Th16;
end;
theorem
Swap(<*p1, p2, p3*>, 1, 3) = <*p3, p2, p1*>
proof
set f = <*p1,p2,p3*>;
A1: len f = 3 by FINSEQ_1:45;
then 1 in dom f by FINSEQ_3:25;
then
A2: f/.1 = f.1 by PARTFUN1:def 6
.= p1;
3 in dom f by A1,FINSEQ_3:25;
then
A3: f/.3 = f.3 by PARTFUN1:def 6
.= p3;
Swap(f,1,3) = Replace(Replace(f,1,f/.3),3,f/.1) by A1,Def2
.= Replace(<*p3,p2,p3*>,3,f/.1) by A3,Th15;
hence thesis by A2,Th17;
end;
theorem
Swap(<*p1, p2, p3*>, 2, 3) = <*p1, p3, p2*>
proof
set f = <*p1,p2,p3*>;
A1: len f = 3 by FINSEQ_1:45;
then 2 in dom f by FINSEQ_3:25;
then
A2: f/.2 = f.2 by PARTFUN1:def 6
.= p2;
3 in dom f by A1,FINSEQ_3:25;
then
A3: f/.3 = f.3 by PARTFUN1:def 6
.= p3;
Swap(f,2,3) = Replace(Replace(f,2,f/.3),3,f/.2) by A1,Def2
.= Replace(<*p1,p3,p3*>,3,f/.2) by A3,Th16;
hence thesis by A2,Th17;
end;
theorem Th27:
1 <= i & i < j & j <= len f implies Swap(f, i, j) = (f|(i-'1))^
<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j)
proof
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f;
A4: i <= len f & 1 <= j by A1,A2,A3,XXREAL_0:2;
Swap(f,i,j) = Swap(f,j,i) by Th21
.= Replace(Replace(f,j,f/.i),i,f/.j) by A1,A3,A4,Def2;
hence thesis by A1,A2,A3,Th11;
end;
theorem
1 < i & i <= len f implies Swap(f, 1, i) = <*f/.i*>^((f/^1)|(i-'2))^<*
f/.1*>^(f/^i)
proof
assume 1 < i & i <= len f; then
Swap(f,1,i) = (f|(1-'1))^<*f/.i*>^(f/^1)|(i-'1-'1)^<*f/.1*>^(f/^i) by Th27
.= (f|0)^<*f/.i*>^(f/^1)|(i-'1-'1)^<*f/.1*>^(f/^i) by XREAL_1:232
.= <*f/.i*>^(f/^1)|(i-'1-'1)^<*f/.1*>^(f/^i) by FINSEQ_1:34;
hence thesis by NAT_D:45;
end;
theorem
1 <= i & i < len f implies Swap(f, i, len f) = (f|(i-'1))^<*f/.len f*>
^((f/^i)|(len f-'i-'1))^<*f/.i*>
proof
assume 1 <= i & i < len f;
then
Swap(f,i,len f) = (f|(i-'1))^<*f/.len f*>^(f/^i)|(len f-'i-'1)^<*f/.i*>^
(f/^len f) by Th27
.= (f|(i-'1))^<*f/.len f*>^(f/^i)|(len f-'i-'1)^<*f/.i*>^{} by RFINSEQ:27;
hence thesis by FINSEQ_1:34;
end;
Lm4: i <> k & j <> k implies Swap(f, i, j).k = f.k
proof
per cases;
suppose
A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
assume that
A2: i <> k and
A3: j <> k;
Replace(Replace(f, i, f/.j), j, f/.i).k = Replace(f, i, f/.j).k by A3,
FUNCT_7:32
.= f.k by A2,FUNCT_7:32;
hence thesis by A1,Def2;
end;
suppose
not (1 <= i & i <= len f & 1 <= j & j <= len f);
hence thesis by Def2;
end;
end;
theorem Th30:
i <> k & j <> k & 1 <= k & k <= len f implies Swap(f, i, j)/.k = f/.k
proof
assume that
A1: i <> k & j <> k and
A2: 1 <= k and
A3: k <= len f;
A4: k in dom f by A2,A3,FINSEQ_3:25;
k <= len Swap(f, i, j) by A3,Th18;
then k in dom Swap(f, i, j) by A2,FINSEQ_3:25;
hence Swap(f, i, j)/.k = Swap(f, i, j).k by PARTFUN1:def 6
.= f.k by A1,Lm4
.= f/.k by A4,PARTFUN1:def 6;
end;
theorem Th31:
1 <= i & i <= len f & 1 <= j & j <= len f implies Swap(f, i, j)
/.i = f/.j & Swap(f, i, j)/.j = f/.i
proof
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f;
A5: i in dom f by A1,A2,FINSEQ_3:25;
set F = Swap(f,i,j);
j <= len F by A4,Th18;
then j in dom F by A3,FINSEQ_3:25;
then
A6: F/.j = F.j by PARTFUN1:def 6
.= f.i by A1,A2,A3,A4,Lm3
.= f/.i by A5,PARTFUN1:def 6;
A7: j in dom f by A3,A4,FINSEQ_3:25;
i <= len F by A2,Th18;
then i in dom F by A1,FINSEQ_3:25;
then F/.i = F.i by PARTFUN1:def 6
.= f.j by A1,A2,A3,A4,Lm3
.= f/.j by A7,PARTFUN1:def 6;
hence thesis by A6;
end;
begin :: Properties of composed function of Replace Function and Swap Function
theorem Th32:
1 <= i & i <= len f & 1 <= j & j <= len f implies Replace(Swap(f
, i, j), i, p) = Swap(Replace(f, j, p), i, j)
proof
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f;
A5: i in dom f by A1,A2,FINSEQ_3:25;
per cases by XXREAL_0:1;
suppose
A6: i = j;
then Replace(Swap(f,i,j),i,p) = Replace(f,i,p) by Th19;
hence thesis by A6,Th19;
end;
suppose
A7: i < j;
set N = <*f/.j*>;
set M = (f|(i-'1));
set F = Swap(f,i,j);
set P = M^N;
A8: F = P^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j) by A1,A4,A7,Th27
.= P^(f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j)) by FINSEQ_1:32
.= P^((f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j))) by FINSEQ_1:32;
set F1 = Replace(f,j,p);
i <= len F1 by A2,FUNCT_7:97;
then
A9: i in dom F1 by A1,FINSEQ_3:25;
A10: f.i = F1.i by A7,FUNCT_7:32
.= F1/.i by A9,PARTFUN1:def 6;
A11: j <= len F1 by A4,FUNCT_7:97;
then
A12: j in dom F1 by A3,FINSEQ_3:25;
set G1 = (f|(j -'1));
A13: j -'1 <= j by NAT_D:35;
A14: i-'1 < j-'1 by A1,A7,NAT_D:56;
then
A15: i -'1 <= len G1 by A4,A13,FINSEQ_1:59,XXREAL_0:2;
set H1 = <*p*>;
set Q = (f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j));
A16: i -'1 <= i by NAT_D:35;
A17: i <= len F by A2,Th18;
len P = len M + len N by FINSEQ_1:22
.= len M + 1 by FINSEQ_1:39
.= i -'1 + 1 by A2,A16,FINSEQ_1:59,XXREAL_0:2
.= i by A1,XREAL_1:235;
then
A18: Replace(F,i,p) = (F|(i-'1))^<*p*>^(F/^len P) by A1,A17,Def1
.= (F|(i-'1))^<*p*>^Q by A8,FINSEQ_5:37
.= ((M^(N^Q))|(i-'1))^<*p*>^Q by A8,FINSEQ_1:32
.= ((M^(N^Q))|len M)^<*p*>^Q by A2,A16,FINSEQ_1:59,XXREAL_0:2
.= M^<*p*>^Q by FINSEQ_5:23;
A19: len (G1^H1) = len G1 + len H1 by FINSEQ_1:22
.= len G1 + 1 by FINSEQ_1:39
.= j -'1 + 1 by A4,A13,FINSEQ_1:59,XXREAL_0:2
.= j by A3,XREAL_1:235;
A20: (F1/^i)|(j-'i-'1) = (F1/^i)|(j-'(i+1)) by NAT_2:30
.= (F1/^i)|(j-'1-'i) by NAT_2:30
.= (F1|(j-'1))/^i by FINSEQ_5:80
.= ((G1^H1^(f/^j))|(j-'1))/^i by A3,A4,Def1
.= ((G1^(H1^(f/^j)))|(j-'1))/^i by FINSEQ_1:32
.= ((G1^(H1^(f/^j)))|len G1)/^i by A4,A13,FINSEQ_1:59,XXREAL_0:2
.= G1/^i by FINSEQ_5:23
.= (f/^i)|((j-'1)-'i) by FINSEQ_5:80
.= (f/^i)|(j-'(1+i)) by NAT_2:30
.= (f/^i)|(j-'i-'1) by NAT_2:30;
A21: p = F1.j by A3,A4,Lm2
.= F1/.j by A12,PARTFUN1:def 6;
A22: F1|(i-'1) = (G1^H1^(f/^j))|(i-'1) by A3,A4,Def1
.= (G1^(H1^(f/^j)))|(i-'1) by FINSEQ_1:32
.= G1|(i-'1) by A15,FINSEQ_5:22
.= f|(i-'1) by A14,FINSEQ_5:77;
A23: F1/^j = (G1^H1^(f/^j))/^j by A3,A4,Def1
.= (f/^j) by A19,FINSEQ_5:37;
Swap(F1,i,j) = (F1|(i-'1))^<*F1/.j*>^(F1/^i)|(j-'i-'1)^<*F1/.i*>^(F1
/^j) by A1,A7,A11,Th27
.= M^<*p*>^(f/^i)|(j-'i-'1)^(<*f.i*>^(f/^j)) by A23,A22,A20,A10,A21,
FINSEQ_1:32
.= M^<*p*>^(f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j)) by A5,PARTFUN1:def 6
.= M^<*p*>^((f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j))) by FINSEQ_1:32;
hence thesis by A18;
end;
suppose
A24: i > j;
then consider k be Nat such that
A25: i = j + k by NAT_1:10;
reconsider i,j,k as Element of NAT by ORDINAL1:def 12;
A26: i - j > j - j by A24,XREAL_1:9;
then
A27: k = i -'j by A25,XREAL_0:def 2;
set X = f/^i;
set W = <*f/.j*>;
set V = (f/^j)|(i-'j-'1);
set N = <*f/.i*>;
set M = (f|(j-'1));
set F = Swap(f,j,i);
set P = M^N;
A28: F = P^V^W^X by A2,A3,A24,Th27
.= P^V^(W^X) by FINSEQ_1:32
.= P^(V^(W^X)) by FINSEQ_1:32
.= P^(V^W^X) by FINSEQ_1:32;
A29: j - 1 >= 1 - 1 by A3,XREAL_1:9;
A30: k+j-'1 = k+j-1 by A25,A26,NAT_1:14,NAT_D:37
.= k+(j-1)
.= k+(j-'1) by A29,XREAL_0:def 2;
A31: k = 1+(k-'1) by A25,A26,NAT_1:14,XREAL_1:235;
set Q = V^W^X;
A32: j -'1 <= j by NAT_D:35;
set F1 = Replace(f,j,p);
set G1 = (f|(j -'1));
A33: j -'1 <= j by NAT_D:35;
set H1 = <*p*>;
j <= len F1 by A4,FUNCT_7:97;
then
A34: j in dom F1 by A3,FINSEQ_3:25;
A35: len (G1^H1) = len G1 + len H1 by FINSEQ_1:22
.= len G1 + 1 by FINSEQ_1:39
.= j -'1 + 1 by A4,A33,FINSEQ_1:59,XXREAL_0:2
.= j by A3,XREAL_1:235;
then
A36: F1/^i = ((G1^H1)^(f/^j))/^(len (G1^H1)+k) by A3,A4,A25,Def1
.= f/^j/^k by FINSEQ_5:36
.= f/^i by A25,FINSEQ_6:81;
k >= 1 by A25,A26,NAT_1:14;
then
A37: k - 1 >= 1 - 1 by XREAL_1:9;
A38: j+k-'1 = j+k-1 by A3,NAT_D:37
.= j+(k-1)
.= j+(k-'1) by A37,XREAL_0:def 2;
A39: i <= len F1 by A2,FUNCT_7:97;
then
A40: i in dom F1 by A1,FINSEQ_3:25;
A41: (F1/^j)|(i-'j-'1) = (F1/^j)|(i-'(j+1)) by NAT_2:30
.= (F1/^j)|(i-'1-'j) by NAT_2:30
.= (F1|(i-'1))/^j by FINSEQ_5:80
.= (((G1^H1)^(f/^j))|(j+(k-'1)))/^j by A3,A4,A25,A38,Def1
.= ((G1^H1)^((f/^j)|(k-'1)))/^len (G1^H1) by A35,GENEALG1:2
.= (f/^j)|(i-'j-'1) by A27,FINSEQ_5:37;
A42: F1|(j-'1) = (G1^H1^(f/^j))|(j-'1) by A3,A4,Def1
.= (G1^(H1^(f/^j)))|(j-'1) by FINSEQ_1:32
.= (G1^(H1^(f/^j)))|len G1 by A4,A33,FINSEQ_1:59,XXREAL_0:2
.= G1 by FINSEQ_5:23;
A43: p = F1.j by A3,A4,Lm2
.= F1/.j by A34,PARTFUN1:def 6;
A44: f.i = F1.i by A24,FUNCT_7:32
.= F1/.i by A40,PARTFUN1:def 6;
A45: Swap(F1,i,j) = Swap(F1,j,i) by Th21
.= (F1|(j-'1))^<*F1/.i*>^(F1/^j)|(i-'j-'1)^<*F1/.j*>^(F1/^i) by A3,A24
,A39,Th27
.= (f|(j-'1))^<*f/.i*>^(f/^j)|(i-'j-'1)^<*p*>^(f/^i) by A5,A36,A42,A41
,A44,A43,PARTFUN1:def 6;
A46: i-'j <> 0 by A26,XREAL_0:def 2;
i -'1 <= i by NAT_D:35;
then i -'1 <= len f by A2,XXREAL_0:2;
then i -'1-'j <= len f -'j by NAT_D:42;
then i -'1-'j <= len (f/^j) by RFINSEQ:29;
then i -'(1+j) <= len (f/^j) by NAT_2:30;
then
A47: i-'j-'1 <= len (f/^j) by NAT_2:30;
then
A48: len V = k-'1 by A27,FINSEQ_1:59;
A49: len P = len M + len N by FINSEQ_1:22
.= len M + 1 by FINSEQ_1:39
.= j -'1 + 1 by A4,A32,FINSEQ_1:59,XXREAL_0:2
.= j by A3,XREAL_1:235;
A50: i <= len F by A2,Th18;
A51: len (V^W) = len V + len W by FINSEQ_1:22
.= len V + 1 by FINSEQ_1:39
.= i-'j-'1 + 1 by A47,FINSEQ_1:59
.= i-'j by A46,NAT_1:14,XREAL_1:235;
Replace(Swap(f,i,j),i,p) = Replace(F,i,p) by Th21
.= (F|(i-'1))^<*p*>^((P^Q)/^(j+k)) by A1,A25,A28,A50,Def1
.= (F|(i-'1))^<*p*>^(((V^W)^X)/^len (V^W)) by A27,A49,A51,FINSEQ_5:36
.= (F|(k+(j-'1)))^<*p*>^X by A25,A30,FINSEQ_5:37
.= ((M^(N^Q))|((j-'1)+k))^<*p*>^X by A28,FINSEQ_1:32
.= ((M^(N^Q))|(len M +k))^<*p*>^X by A4,A32,FINSEQ_1:59,XXREAL_0:2
.= (M^((N^Q)|k))^<*p*>^X by GENEALG1:2
.= (M^((N^Q)|(len N+(k-'1))))^<*p*>^X by A31,FINSEQ_1:39
.= (M^(N^(Q|(k-'1))))^<*p*>^X by GENEALG1:2
.= (M^(N^((V^(W^X))|(k-'1))))^<*p*>^X by FINSEQ_1:32
.= (M^(N^V))^<*p*>^X by A48,FINSEQ_5:23
.= (M^N^V)^<*p*>^X by FINSEQ_1:32;
hence thesis by A45;
end;
end;
theorem Th33:
i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f
implies Swap(Replace(f, k, p), i, j) = Replace(Swap(f, i, j), k, p)
proof
assume that
A1: i <> k and
A2: j <> k and
A3: 1 <= i and
A4: i <= len f and
A5: 1 <= j and
A6: j <= len f;
i <= len Replace(f, k, p) & j <= len Replace(f, k, p) by A4,A6,FUNCT_7:97;
hence Swap(Replace(f, k, p), i, j) = Replace(Replace(Replace(f, k, p), i,
Replace(f, k, p)/.j), j, Replace(f, k, p)/.i) by A3,A5,Def2
.= Replace(Replace( Replace(f, k, p), i, f/.j), j, Replace(f, k, p)/.i)
by A2,A5,A6,Th10
.= Replace(Replace(Replace(f, k, p), i, f/.j), j, f/.i) by A1,A3,A4,Th10
.= Replace(Replace(Replace(f, i, f/.j), k, p), j, f/.i) by A1,FUNCT_7:33
.= Replace(Replace(Replace(f, i, f/.j), j, f/.i), k, p) by A2,FUNCT_7:33
.= Replace(Swap(f, i, j), k, p) by A3,A4,A5,A6,Def2;
end;
theorem
i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k &
k <= len f implies Swap(Swap(f, i, j), j, k) = Swap(Swap(f, i, k), i, j)
proof
assume that
A1: i <> k & j <> k and
A2: 1 <= i and
A3: i <= len f and
A4: 1 <= j and
A5: j <= len f and
A6: 1 <= k and
A7: k <= len f;
A8: i <= len Replace(f, i, f/.k) & j <= len Replace(f, i, f/.k) by A3,A5,
FUNCT_7:97;
j <= len Swap(f, i, j) & k <= len Swap(f, i, j) by A5,A7,Th18;
hence
Swap(Swap(f, i, j), j, k) = Replace(Replace(Swap(f, i, j), j, Swap(f, i
, j)/.k), k, Swap(f, i, j)/.j) by A4,A6,Def2
.= Replace(Replace(Swap(f, i, j), j, Swap(f, i, j)/.k), k, f/.i) by A2,A3
,A4,A5,Th31
.= Replace(Replace(Swap(f, i, j), j, f/.k), k, f/.i) by A1,A6,A7,Th30
.= Replace(Replace(Swap(f, j, i), j, f/.k), k, f/.i) by Th21
.= Replace(Swap(Replace(f, i, f/.k), j, i), k, f/.i) by A2,A3,A4,A5,Th32
.= Swap(Replace(Replace(f, i, f/.k), k, f/.i), j, i) by A1,A2,A4,A8,Th33
.= Swap(Swap(f, i, k), j, i) by A2,A3,A6,A7,Def2
.= Swap(Swap(f, i, k), i, j) by Th21;
end;
theorem
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 implies Swap(Swap(f, i, j)
, k, l) = Swap(Swap(f, k, l), i, j)
proof
assume that
A1: i <> k & j <> k and
A2: l <> i & l <> j and
A3: 1 <= i and
A4: i <= len f and
A5: 1 <= j and
A6: j <= len f and
A7: 1 <= k and
A8: k <= len f and
A9: 1 <= l and
A10: l <= len f;
A11: i <= len Replace(f,k,f/.l) & j <= len Replace(f,k,f/.l)
by A4,A6,FUNCT_7:97;
set F = Swap(f,i,j);
k <= len F & l <= len F by A8,A10,Th18;
then Swap(F,k,l) = Replace(Replace(F,k,F/.l),l,F/.k) by A7,A9,Def2
.= Replace(Replace(F,k,F/.l),l,f/.k) by A1,A7,A8,Th30
.= Replace(Replace(F,k,f/.l),l,f/.k) by A2,A9,A10,Th30
.= Replace(Replace(Swap(f,j,i),k,f/.l),l,f/.k) by Th21
.= Replace(Swap(Replace(f,k,f/.l),j,i),l,f/.k) by A1,A3,A4,A5,A6,Th33
.= Swap(Replace(Replace(f,k,f/.l),l,f/.k),j,i) by A2,A3,A5,A11,Th33
.= Swap(Swap(f,k,l),j,i) by A7,A8,A9,A10,Def2
.= Swap(Swap(f,k,l),i,j) by Th21;
hence thesis;
end;