per cases ( not p in rng f or p in rng f ) ;
suppose not p in rng f ; :: thesis: not Rotate (f,p) is constant
hence not Rotate (f,p) is constant by Def2; :: thesis: verum
end;
suppose A1: p in rng f ; :: thesis: not Rotate (f,p) is constant
A2: dom (Rotate (f,p)) = dom f by Th15;
consider n, m being Nat such that
A3: n in dom f and
A4: m in dom f and
A5: f /. n <> f /. m by Def1;
A6: n <= len f by ;
A7: m <= len f by ;
A8: 1 <= m by ;
A9: 1 <= n by ;
thus Rotate (f,p) is V25() :: thesis: verum
proof
A10: 1 <= p .. f by ;
A11: p .. f <= len f by ;
per cases ( ( n <= p .. f & m <= p .. f ) or ( n <= p .. f & m >= p .. f ) or ( m <= p .. f & n >= p .. f ) or ( m >= p .. f & n >= p .. f ) ) ;
suppose that A12: n <= p .. f and
A13: m <= p .. f ; :: thesis: Rotate (f,p) is V25()
n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by ;
then A14: 1 <= (n + (len f)) -' (p .. f) by ;
m <= m + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= m + ((len f) -' (p .. f)) by ;
then A15: 1 <= (m + (len f)) -' (p .. f) by ;
m + (len f) <= (len f) + (p .. f) by ;
then (m + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A16: (m + (len f)) -' (p .. f) in dom f by ;
n + (len f) <= (len f) + (p .. f) by ;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A17: (n + (len f)) -' (p .. f) in dom f by ;
( f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) & f /. m = (Rotate (f,p)) /. ((m + (len f)) -' (p .. f)) ) by A1, A9, A8, A12, A13, Th18;
hence Rotate (f,p) is V25() by A5, A2, A17, A16; :: thesis: verum
end;
suppose that A18: n <= p .. f and
A19: m >= p .. f ; :: thesis: Rotate (f,p) is V25()
1 + (p .. f) <= m + 1 by ;
then A20: 1 <= (m + 1) -' (p .. f) by NAT_D:55;
n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by ;
then A21: 1 <= (n + (len f)) -' (p .. f) by ;
n + (len f) <= (len f) + (p .. f) by ;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A22: (n + (len f)) -' (p .. f) in dom f by ;
m + 1 <= (len f) + (p .. f) by ;
then (m + 1) -' (p .. f) <= len f by NAT_D:53;
then A23: (m + 1) -' (p .. f) in dom f by ;
( f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) & f /. m = (Rotate (f,p)) /. ((m + 1) -' (p .. f)) ) by A1, A9, A7, A18, A19, Th10, Th18;
hence Rotate (f,p) is V25() by A5, A2, A22, A23; :: thesis: verum
end;
suppose that A24: m <= p .. f and
A25: n >= p .. f ; :: thesis: Rotate (f,p) is V25()
1 + (p .. f) <= n + 1 by ;
then A26: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
m <= m + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= m + ((len f) -' (p .. f)) by ;
then A27: 1 <= (m + (len f)) -' (p .. f) by ;
m + (len f) <= (len f) + (p .. f) by ;
then (m + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A28: (m + (len f)) -' (p .. f) in dom f by ;
n + 1 <= (len f) + (p .. f) by ;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then A29: (n + 1) -' (p .. f) in dom f by ;
( f /. m = (Rotate (f,p)) /. ((m + (len f)) -' (p .. f)) & f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) ) by A1, A6, A8, A24, A25, Th10, Th18;
hence Rotate (f,p) is V25() by A5, A2, A28, A29; :: thesis: verum
end;
suppose that A30: m >= p .. f and
A31: n >= p .. f ; :: thesis: Rotate (f,p) is V25()
1 + (p .. f) <= m + 1 by ;
then A32: 1 <= (m + 1) -' (p .. f) by NAT_D:55;
1 + (p .. f) <= n + 1 by ;
then A33: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
n + 1 <= (len f) + (p .. f) by ;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then A34: (n + 1) -' (p .. f) in dom f by ;
m + 1 <= (len f) + (p .. f) by ;
then (m + 1) -' (p .. f) <= len f by NAT_D:53;
then A35: (m + 1) -' (p .. f) in dom f by ;
( f /. m = (Rotate (f,p)) /. ((m + 1) -' (p .. f)) & f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) ) by A1, A6, A7, A30, A31, Th10;
hence Rotate (f,p) is V25() by A5, A2, A35, A34; :: thesis: verum
end;
end;
end;
end;
end;