[isabelle] Datatypes questions with use case



I am still stuck with datatypes.

I need a set function, which is able to do the following:

   - Have topological connection between several things, showing that they
   have equivalent behavior - for (in example here) projecting the natural
   numbers sequence to itself (to show that some properties have some
   irrelevance to how small or big the numbers are).
   - Actually explain it, what I do - not just by defining two functions,
   which are provably similar, but showing that if one exits, then another must
   finish with a smaller number.
   - Have the sequence, which allows to use >-kind operator to check if some
   number follows another (the question is not about operator, but about having
   the functionality - it currently tries to start with proving that the set is
   monotone, but this is where this thing must lead and this has not been
   proven yet, thus I can't start defining thing needed to prove that it is
   from some fast-automatic-check checking if it is, but I need another way for
   that).

Also, I would be happy for a few simple proofs about math, which do not use
assign-type syntax, but the kind of syntax described in short Isar manual -
I really like that syntax, because I can understand that and I think that I
might slowly learn to use that other, too (because it's clearly sometimes
convenient), but much more I would like to be able to read the proofs
afterwards. Thus, examples using that syntax would be very good thing to
have (with natural numbers and preferably some about binary numbers, too).


Below is mostly everything I need to show as starting point, also there is
Python file containing the configurable code, which generated that:

Legend:
pp1(n) = how many times the number minus 1 (n-1) divides by 2
pm3d2(n) = how many times (3n+1)/2 divides by 2
pm3(n) = how many times (3n+1) divides by 2.
subc(n)* = (n-1)/2; notice the sub-collatzes in regards to pp1(n).

* For subc, there are approximations, because the exact divisibility and
rounding is actually synchronized to exact numbers and done in several
steps,
which take into consideration the divisibility of previous number. Anyway,
this formula is useful in understanding the Collatz function. This is
showable
from fractal, that subc*0.75 actually rounds up (as all other calls also do,
which
is not visible from number circle ) - because number spiral
is loosing some intermediate positions between numbers, which are divisable
by bigger numbers.

Explanation:
pp1(n) = how many times to do n=n*1.5.
pm3(n) = how many times to do n/2 afterwards.
subc(n) = how many times the Collatz plays that it's Collatz with smaller
numbers, before zooming out to equivalent position.

Notice the fractal pattern [0102010301020104...] and it's variations!

Numbers make up a nice structure (only a
few members of Collatz series are here - those, which are
involved in pattern); only odd numbers are presented as Collatz
normalizes each number to odd as a first thing:

pp1(n+1)=  2 /\ n=  3 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [3, 5, 8, 4,
2, 1]
  [010*010301020104010201030102010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n=  5 /\ pm3d2(n)=  3 /\ pm3(n)=  4 /\ Seq(n) = [5, 8, 4, 2,
1]
  [01020*0301020104010201030102010501020103010201040102010301020106]
pp1(n+1)=  3 /\ n=  7 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [7, 11, 17,
26, 13, 20, 10, 5, 8..]
  [0102010*01020104010201030102010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n=  9 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [9, 14, 7,
11, 17, 26, 13, 20, 10..]
  [010201030*020104010201030102010501020103010201040102010301020106]
pp1(n+1)=  2 /\ n= 11 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [11, 17, 26,
13, 20, 10, 5, 8, 4..]
  [01020103010*0104010201030102010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n= 13 /\ pm3d2(n)=  2 /\ pm3(n)=  3 /\ Seq(n) = [13, 20, 10,
5, 8, 4, 2, 1]
  [0102010301020*04010201030102010501020103010201040102010301020106]
pp1(n+1)=  4 /\ n= 15 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [15, 23, 35,
53, 80, 40, 20, 10, 5..]
  [010201030102010*010201030102010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n= 17 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [17, 26, 13,
20, 10, 5, 8, 4, 2..]
  [01020103010201040*0201030102010501020103010201040102010301020106]
pp1(n+1)=  2 /\ n= 19 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [19, 29, 44,
22, 11, 17, 26, 13, 20..]
  [0102010301020104010*01030102010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n= 21 /\ pm3d2(n)=  5 /\ pm3(n)=  6 /\ Seq(n) = [21, 32, 16,
8, 4, 2, 1]
  [010201030102010401020*030102010501020103010201040102010301020106]
pp1(n+1)=  3 /\ n= 23 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [23, 35, 53,
80, 40, 20, 10, 5, 8..]
  [01020103010201040102010*0102010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n= 25 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [25, 38, 19,
29, 44, 22, 11, 17, 26..]
  [0102010301020104010201030*02010501020103010201040102010301020106]
pp1(n+1)=  2 /\ n= 27 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [27, 41, 62,
31, 47, 71, 107, 161, 242..]
  [010201030102010401020103010*010501020103010201040102010301020106]
pp1(n+1)=  1 /\ n= 29 /\ pm3d2(n)=  2 /\ pm3(n)=  3 /\ Seq(n) = [29, 44, 22,
11, 17, 26, 13, 20, 10..]
  [01020103010201040102010301020*0501020103010201040102010301020106]
pp1(n+1)=  5 /\ n= 31 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [31, 47, 71,
107, 161, 242, 121, 182, 91..]
  [0102010301020104010201030102010*01020103010201040102010301020106]
pp1(n+1)=  1 /\ n= 33 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [33, 50, 25,
38, 19, 29, 44, 22, 11..]
  [010201030102010401020103010201050*020103010201040102010301020106]
pp1(n+1)=  2 /\ n= 35 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [35, 53, 80,
40, 20, 10, 5, 8, 4..]
  [01020103010201040102010301020105010*0103010201040102010301020106]
pp1(n+1)=  1 /\ n= 37 /\ pm3d2(n)=  3 /\ pm3(n)=  4 /\ Seq(n) = [37, 56, 28,
14, 7, 11, 17, 26, 13..]
  [0102010301020104010201030102010501020*03010201040102010301020106]
pp1(n+1)=  3 /\ n= 39 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [39, 59, 89,
134, 67, 101, 152, 76, 38..]
  [010201030102010401020103010201050102010*010201040102010301020106]
pp1(n+1)=  1 /\ n= 41 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [41, 62, 31,
47, 71, 107, 161, 242, 121..]
  [01020103010201040102010301020105010201030*0201040102010301020106]
pp1(n+1)=  2 /\ n= 43 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [43, 65, 98,
49, 74, 37, 56, 28, 14..]
  [0102010301020104010201030102010501020103010*01040102010301020106]
pp1(n+1)=  1 /\ n= 45 /\ pm3d2(n)=  2 /\ pm3(n)=  3 /\ Seq(n) = [45, 68, 34,
17, 26, 13, 20, 10, 5..]
  [010201030102010401020103010201050102010301020*040102010301020106]
pp1(n+1)=  4 /\ n= 47 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [47, 71,
107, 161, 242, 121, 182, 91, 137..]
  [01020103010201040102010301020105010201030102010*0102010301020106]
pp1(n+1)=  1 /\ n= 49 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [49, 74, 37,
56, 28, 14, 7, 11, 17..]
pp1(n+1)=  2 /\ n= 51 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [51, 77,
116, 58, 29, 44, 22, 11, 17..]
pp1(n+1)=  1 /\ n= 53 /\ pm3d2(n)=  4 /\ pm3(n)=  5 /\ Seq(n) = [53, 80, 40,
20, 10, 5, 8, 4, 2..]
pp1(n+1)=  3 /\ n= 55 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [55, 83,
125, 188, 94, 47, 71, 107, 161..]
pp1(n+1)=  1 /\ n= 57 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [57, 86, 43,
65, 98, 49, 74, 37, 56..]
pp1(n+1)=  2 /\ n= 59 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [59, 89,
134, 67, 101, 152, 76, 38, 19..]
pp1(n+1)=  1 /\ n= 61 /\ pm3d2(n)=  2 /\ pm3(n)=  3 /\ Seq(n) = [61, 92, 46,
23, 35, 53, 80, 40, 20..]
pp1(n+1)=  6 /\ n= 63 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [63, 95,
143, 215, 323, 485, 728, 364, 182..]
pp1(n+1)=  1 /\ n= 65 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [65, 98, 49,
74, 37, 56, 28, 14, 7..]
pp1(n+1)=  2 /\ n= 67 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [67, 101,
152, 76, 38, 19, 29, 44, 22..]
pp1(n+1)=  1 /\ n= 69 /\ pm3d2(n)=  3 /\ pm3(n)=  4 /\ Seq(n) = [69, 104,
52, 26, 13, 20, 10, 5, 8..]
pp1(n+1)=  3 /\ n= 71 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [71, 107,
161, 242, 121, 182, 91, 137, 206..]
pp1(n+1)=  1 /\ n= 73 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [73, 110,
55, 83, 125, 188, 94, 47, 71..]
pp1(n+1)=  2 /\ n= 75 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [75, 113,
170, 85, 128, 64, 32, 16, 8..]
pp1(n+1)=  1 /\ n= 77 /\ pm3d2(n)=  2 /\ pm3(n)=  3 /\ Seq(n) = [77, 116,
58, 29, 44, 22, 11, 17, 26..]
pp1(n+1)=  4 /\ n= 79 /\ pm3d2(n)=  0 /\ pm3(n)=  1 /\ Seq(n) = [79, 119,
179, 269, 404, 202, 101, 152, 76..]
pp1(n+1)=  1 /\ n= 81 /\ pm3d2(n)=  1 /\ pm3(n)=  2 /\ Seq(n) = [81, 122,
61, 92, 46, 23, 35, 53, 80..]

Here, the pattern of divisions (things between counting to 1 and after two
of them) need a little explanation.

Look at this sequence of divisibility:
  [0102010301020104010201030102010501020103010201040102010301020106]

For understanding the sequence each time Collatz reaches a point,
imagine the point being adjusted so that if biggest number right
before the number is 4, then take the position from first 4 and
adjust it so that it's the same in regards to first 2:


Patterns for 5:
          [0102*10301020104010201030102010501020103010201040102010301020106]
      5   [0102*10301020104010201030102010501020103010201040102010301020106]
      8*  [0102010*01020104010201030102010501020103010201040102010301020106]
      4   [010*010301020104010201030102010501020103010201040102010301020106]
      2   [0*02010301020104010201030102010501020103010201040102010301020106]
      1   [*102010301020104010201030102010501020103010201040102010301020106]

Here it's visible, how Collatz changes. It will actually
use a formula 'pow(3, times) * (number + 1) / pow(2, times) - 1' to decide,
how many times to do 3n+1. Times = maxp2(number+1), which is maximum power
of two, by which the number can be divided. We see that it's like reverse
operation to division by two. This means - it uses the next position of a
number and replaces 2's with 3' in it's prime components.

Here, we are primarily interested in how it proceeds _down_ - as we see, if
it's on such position that no number before it has equal (or bigger) maxp2
value, then it proceeds to previous such position with maxp2-1.
Patterns for 7:
          [010201*301020104010201030102010501020103010201040102010301020106]
      7*  [010201*301020104010201030102010501020103010201040102010301020106]
     11   [0102010301*20104010201030102010501020103010201040102010301020106]
     17   [0102010301020104*10201030102010501020103010201040102010301020106]
     26   [0102010301020104010201030*02010501020103010201040102010301020106]
     13   [010201030102*104010201030102010501020103010201040102010301020106]
     20*  [0102010301020104010*01030102010501020103010201040102010301020106]
     10   [010201030*020104010201030102010501020103010201040102010301020106]
      5   [0102*10301020104010201030102010501020103010201040102010301020106]
      8*  [0102010*01020104010201030102010501020103010201040102010301020106]
      4   [010*010301020104010201030102010501020103010201040102010301020106]
      2   [0*02010301020104010201030102010501020103010201040102010301020106]
      1   [*102010301020104010201030102010501020103010201040102010301020106]

This gets more interesting as it involves upwards movement. We
see, how it targets biggest power of two after it - such tendence comes from
how the pyramid of prime component 2 in n is synchronized with the same in
n + 1. We can say that collatz is built from two entangled variables - S, N.
N = S+1. N[2] is number of twos in N's prime components, S[2] the same for S
and N[3] the number of threes. Collatz will be, then:

Loop:
  S[2] = 0
  N[3] = N[2]
  N[2] = 0

The exact movement strategy becomes visible by imagining 3S+1 as
round_up(N*1.5).

Patterns for 19:
          [010201030102010401*201030102010501020103010201040102010301020106]
     19   [010201030102010401*201030102010501020103010201040102010301020106]
     29   [0102010301020104010201030102*10501020103010201040102010301020106]
     11   [0102010301*20104010201030102010501020103010201040102010301020106]
     17   [0102010301020104*10201030102010501020103010201040102010301020106]
     26   [0102010301020104010201030*02010501020103010201040102010301020106]
     13   [010201030102*104010201030102010501020103010201040102010301020106]
     10   [010201030*020104010201030102010501020103010201040102010301020106]
      5   [0102*10301020104010201030102010501020103010201040102010301020106]
      4   [010*010301020104010201030102010501020103010201040102010301020106]
      2   [0*02010301020104010201030102010501020103010201040102010301020106]
      1   [*102010301020104010201030102010501020103010201040102010301020106]

This a-bit-larger-scale movement (the same number in another
format follows right here).
19[pp1:2;pm3:1;subc:9{c(9)=14}]
29[pp1:1;pm3:3;subc:14{*0.75~=10}] 44 22
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

13-5 is the *0.75 operation of subc (subc=(n-1)/2),
which basically moves us to another position with equivalent surroundings.
As
we know the exact manner, how Collatz moves there - using parity of N as
hint
if it's needed to move further by 1/2 of current position, we can see that
the topology does not change by this operation - it repeats the same upwards
seek operation (add 1/2 as long as S is odd and N is even, which equals to
maxp2(N)), we can see, why it prefers to go to position right after the
biggest
maxp2 nearby. This text here has also explained some symmetries of Collatz
function, which are enough to prove it as I believe:

1. The function replicates itself in each of it's step, thus the replication
itself replicates itself.
2. This is simply describable, how it "zooms in" to number sequence exactly
when 0.75 actually gives the equivalent position.
3. This allows to show that it repeats itself in itself.

This is a few series written out for better understanding:
pp1(n+1)=  2 /\ n=  3 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=2 times in a row, result will
be 21.
pp1(n) will count to one.

3[pp1:2;pm3:1;subc:1{c(1)=1}]
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n=  5 /\ pm3d2(n)=  3 /\ pm3(n)=  4
The operation n/2 will be done pm3d2(n)=3 times in a row after one (3n+1),
result will be 1.
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  3 /\ n=  7 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=3 times in a row, result will
be 73.
pp1(n) will count to one.

7[pp1:3;pm3:1;subc:3{c(3)=5}]
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n=  9 /\ pm3d2(n)=  1 /\ pm3(n)=  2
The operation n/2 will be done pm3d2(n)=1 times in a row after one (3n+1),
result will be 7.
9[pp1:1;pm3:2;subc:4{*0.75~=3}] 14
7[pp1:3;pm3:1;subc:3{c(3)=5}]
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  2 /\ n= 11 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=2 times in a row, result will
be 75.
pp1(n) will count to one.

11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 13 /\ pm3d2(n)=  2 /\ pm3(n)=  3
The operation n/2 will be done pm3d2(n)=2 times in a row after one (3n+1),
result will be 5.
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  4 /\ n= 15 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=4 times in a row, result will
be 231.
pp1(n) will count to one.

15[pp1:4;pm3:1;subc:7{c(7)=11}]
23[pp1:3;pm3:1;subc:11{c(11)=17}]
35[pp1:2;pm3:1;subc:17{c(17)=26}]
53[pp1:1;pm3:5;subc:26{*0.75~=19}] 80 40 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 17 /\ pm3d2(n)=  1 /\ pm3(n)=  2
The operation n/2 will be done pm3d2(n)=1 times in a row after one (3n+1),
result will be 13.
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  2 /\ n= 19 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=2 times in a row, result will
be 129.
pp1(n) will count to one.

19[pp1:2;pm3:1;subc:9{c(9)=14}]
29[pp1:1;pm3:3;subc:14{*0.75~=10}] 44 22
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 21 /\ pm3d2(n)=  5 /\ pm3(n)=  6
The operation n/2 will be done pm3d2(n)=5 times in a row after one (3n+1),
result will be 1.
21[pp1:1;pm3:6;subc:10{*0.75~=7}] 32 16 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  3 /\ n= 23 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=3 times in a row, result will
be 235.
pp1(n) will count to one.

23[pp1:3;pm3:1;subc:11{c(11)=17}]
35[pp1:2;pm3:1;subc:17{c(17)=26}]
53[pp1:1;pm3:5;subc:26{*0.75~=19}] 80 40 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 25 /\ pm3d2(n)=  1 /\ pm3(n)=  2
The operation n/2 will be done pm3d2(n)=1 times in a row after one (3n+1),
result will be 19.
25[pp1:1;pm3:2;subc:12{*0.75~=9}] 38
19[pp1:2;pm3:1;subc:9{c(9)=14}]
29[pp1:1;pm3:3;subc:14{*0.75~=10}] 44 22
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  2 /\ n= 27 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=2 times in a row, result will
be 183.
pp1(n) will count to one.

27[pp1:2;pm3:1;subc:13{c(13)=20}]
41[pp1:1;pm3:2;subc:20{*0.75~=15}] 62
31[pp1:5;pm3:1;subc:15{c(15)=23}]
47[pp1:4;pm3:1;subc:23{c(23)=35}]
71[pp1:3;pm3:1;subc:35{c(35)=53}]
107[pp1:2;pm3:1;subc:53{c(53)=80}]
161[pp1:1;pm3:2;subc:80{*0.75/2~=30}] 242
121[pp1:1;pm3:2;subc:60{*0.75~=45}] 182
91[pp1:2;pm3:1;subc:45{c(45)=68}]
137[pp1:1;pm3:2;subc:68{*0.75~=51}] 206
103[pp1:3;pm3:1;subc:51{c(51)=77}]
155[pp1:2;pm3:1;subc:77{c(77)=116}]
233[pp1:1;pm3:2;subc:116{*0.75~=87}] 350
175[pp1:4;pm3:1;subc:87{c(87)=131}]
263[pp1:3;pm3:1;subc:131{c(131)=197}]
395[pp1:2;pm3:1;subc:197{c(197)=296}]
593[pp1:1;pm3:2;subc:296{*0.75~=222}] 890
445[pp1:1;pm3:3;subc:222{*0.75~=166}] 668 334
167[pp1:3;pm3:1;subc:83{c(83)=125}]
251[pp1:2;pm3:1;subc:125{c(125)=188}]
377[pp1:1;pm3:2;subc:188{*0.75~=141}] 566
283[pp1:2;pm3:1;subc:141{c(141)=212}]
425[pp1:1;pm3:2;subc:212{*0.75~=159}] 638
319[pp1:6;pm3:1;subc:159{c(159)=239}]
479[pp1:5;pm3:1;subc:239{c(239)=359}]
719[pp1:4;pm3:1;subc:359{c(359)=539}]
1079[pp1:3;pm3:1;subc:539{c(539)=809}]
1619[pp1:2;pm3:1;subc:809{c(809)=1214}]
2429[pp1:1;pm3:3;subc:1214{*0.75~=910}] 3644 1822
911[pp1:4;pm3:1;subc:455{c(455)=683}]
1367[pp1:3;pm3:1;subc:683{c(683)=1025}]
2051[pp1:2;pm3:1;subc:1025{c(1025)=1538}]
3077[pp1:1;pm3:4;subc:1538{*0.75~=1153}] 4616 2308 1154
577[pp1:1;pm3:2;subc:288{*0.75/4~=54}] 866
433[pp1:1;pm3:2;subc:216{*0.75~=162}] 650
325[pp1:1;pm3:4;subc:162{*0.75~=121}] 488 244 122
61[pp1:1;pm3:3;subc:30{*0.75~=22}] 92 46
23[pp1:3;pm3:1;subc:11{c(11)=17}]
35[pp1:2;pm3:1;subc:17{c(17)=26}]
53[pp1:1;pm3:5;subc:26{*0.75~=19}] 80 40 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 29 /\ pm3d2(n)=  2 /\ pm3(n)=  3
The operation n/2 will be done pm3d2(n)=2 times in a row after one (3n+1),
result will be 11.
29[pp1:1;pm3:3;subc:14{*0.75~=10}] 44 22
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  5 /\ n= 31 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=5 times in a row, result will
be 712.
pp1(n) will count to one.

31[pp1:5;pm3:1;subc:15{c(15)=23}]
47[pp1:4;pm3:1;subc:23{c(23)=35}]
71[pp1:3;pm3:1;subc:35{c(35)=53}]
107[pp1:2;pm3:1;subc:53{c(53)=80}]
161[pp1:1;pm3:2;subc:80{*0.75/2~=30}] 242
121[pp1:1;pm3:2;subc:60{*0.75~=45}] 182
91[pp1:2;pm3:1;subc:45{c(45)=68}]
137[pp1:1;pm3:2;subc:68{*0.75~=51}] 206
103[pp1:3;pm3:1;subc:51{c(51)=77}]
155[pp1:2;pm3:1;subc:77{c(77)=116}]
233[pp1:1;pm3:2;subc:116{*0.75~=87}] 350
175[pp1:4;pm3:1;subc:87{c(87)=131}]
263[pp1:3;pm3:1;subc:131{c(131)=197}]
395[pp1:2;pm3:1;subc:197{c(197)=296}]
593[pp1:1;pm3:2;subc:296{*0.75~=222}] 890
445[pp1:1;pm3:3;subc:222{*0.75~=166}] 668 334
167[pp1:3;pm3:1;subc:83{c(83)=125}]
251[pp1:2;pm3:1;subc:125{c(125)=188}]
377[pp1:1;pm3:2;subc:188{*0.75~=141}] 566
283[pp1:2;pm3:1;subc:141{c(141)=212}]
425[pp1:1;pm3:2;subc:212{*0.75~=159}] 638
319[pp1:6;pm3:1;subc:159{c(159)=239}]
479[pp1:5;pm3:1;subc:239{c(239)=359}]
719[pp1:4;pm3:1;subc:359{c(359)=539}]
1079[pp1:3;pm3:1;subc:539{c(539)=809}]
1619[pp1:2;pm3:1;subc:809{c(809)=1214}]
2429[pp1:1;pm3:3;subc:1214{*0.75~=910}] 3644 1822
911[pp1:4;pm3:1;subc:455{c(455)=683}]
1367[pp1:3;pm3:1;subc:683{c(683)=1025}]
2051[pp1:2;pm3:1;subc:1025{c(1025)=1538}]
3077[pp1:1;pm3:4;subc:1538{*0.75~=1153}] 4616 2308 1154
577[pp1:1;pm3:2;subc:288{*0.75/4~=54}] 866
433[pp1:1;pm3:2;subc:216{*0.75~=162}] 650
325[pp1:1;pm3:4;subc:162{*0.75~=121}] 488 244 122
61[pp1:1;pm3:3;subc:30{*0.75~=22}] 92 46
23[pp1:3;pm3:1;subc:11{c(11)=17}]
35[pp1:2;pm3:1;subc:17{c(17)=26}]
53[pp1:1;pm3:5;subc:26{*0.75~=19}] 80 40 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 33 /\ pm3d2(n)=  1 /\ pm3(n)=  2
The operation n/2 will be done pm3d2(n)=1 times in a row after one (3n+1),
result will be 25.
33[pp1:1;pm3:2;subc:16{*0.75/2~=6}] 50
25[pp1:1;pm3:2;subc:12{*0.75~=9}] 38
19[pp1:2;pm3:1;subc:9{c(9)=14}]
29[pp1:1;pm3:3;subc:14{*0.75~=10}] 44 22
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  2 /\ n= 35 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=2 times in a row, result will
be 237.
pp1(n) will count to one.

35[pp1:2;pm3:1;subc:17{c(17)=26}]
53[pp1:1;pm3:5;subc:26{*0.75~=19}] 80 40 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 37 /\ pm3d2(n)=  3 /\ pm3(n)=  4
The operation n/2 will be done pm3d2(n)=3 times in a row after one (3n+1),
result will be 7.
37[pp1:1;pm3:4;subc:18{*0.75~=13}] 56 28 14
7[pp1:3;pm3:1;subc:3{c(3)=5}]
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  3 /\ n= 39 /\ pm3d2(n)=  0 /\ pm3(n)=  1
The operation (3n+1)/2 will be done pp1(n+1)=3 times in a row, result will
be 397.
pp1(n) will count to one.

39[pp1:3;pm3:1;subc:19{c(19)=29}]
59[pp1:2;pm3:1;subc:29{c(29)=44}]
89[pp1:1;pm3:2;subc:44{*0.75~=33}] 134
67[pp1:2;pm3:1;subc:33{c(33)=50}]
101[pp1:1;pm3:4;subc:50{*0.75~=37}] 152 76 38
19[pp1:2;pm3:1;subc:9{c(9)=14}]
29[pp1:1;pm3:3;subc:14{*0.75~=10}] 44 22
11[pp1:2;pm3:1;subc:5{c(5)=8}]
17[pp1:1;pm3:2;subc:8{*0.75~=6}] 26
13[pp1:1;pm3:3;subc:6{*0.75/2~=2}] 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

pp1(n+1)=  1 /\ n= 41 /\ pm3d2(n)=  1 /\ pm3(n)=  2
The operation n/2 will be done pm3d2(n)=1 times in a row after one (3n+1),
result will be 31.
41[pp1:1;pm3:2;subc:20{*0.75~=15}] 62
31[pp1:5;pm3:1;subc:15{c(15)=23}]
47[pp1:4;pm3:1;subc:23{c(23)=35}]
71[pp1:3;pm3:1;subc:35{c(35)=53}]
107[pp1:2;pm3:1;subc:53{c(53)=80}]
161[pp1:1;pm3:2;subc:80{*0.75/2~=30}] 242
121[pp1:1;pm3:2;subc:60{*0.75~=45}] 182
91[pp1:2;pm3:1;subc:45{c(45)=68}]
137[pp1:1;pm3:2;subc:68{*0.75~=51}] 206
103[pp1:3;pm3:1;subc:51{c(51)=77}]
155[pp1:2;pm3:1;subc:77{c(77)=116}]
233[pp1:1;pm3:2;subc:116{*0.75~=87}] 350
175[pp1:4;pm3:1;subc:87{c(87)=131}]
263[pp1:3;pm3:1;subc:131{c(131)=197}]
395[pp1:2;pm3:1;subc:197{c(197)=296}]
593[pp1:1;pm3:2;subc:296{*0.75~=222}] 890
445[pp1:1;pm3:3;subc:222{*0.75~=166}] 668 334
167[pp1:3;pm3:1;subc:83{c(83)=125}]
251[pp1:2;pm3:1;subc:125{c(125)=188}]
377[pp1:1;pm3:2;subc:188{*0.75~=141}] 566
283[pp1:2;pm3:1;subc:141{c(141)=212}]
425[pp1:1;pm3:2;subc:212{*0.75~=159}] 638
319[pp1:6;pm3:1;subc:159{c(159)=239}]
479[pp1:5;pm3:1;subc:239{c(239)=359}]
719[pp1:4;pm3:1;subc:359{c(359)=539}]
1079[pp1:3;pm3:1;subc:539{c(539)=809}]
1619[pp1:2;pm3:1;subc:809{c(809)=1214}]
2429[pp1:1;pm3:3;subc:1214{*0.75~=910}] 3644 1822
911[pp1:4;pm3:1;subc:455{c(455)=683}]
1367[pp1:3;pm3:1;subc:683{c(683)=1025}]
2051[pp1:2;pm3:1;subc:1025{c(1025)=1538}]
3077[pp1:1;pm3:4;subc:1538{*0.75~=1153}] 4616 2308 1154
577[pp1:1;pm3:2;subc:288{*0.75/4~=54}] 866
433[pp1:1;pm3:2;subc:216{*0.75~=162}] 650
325[pp1:1;pm3:4;subc:162{*0.75~=121}] 488 244 122
61[pp1:1;pm3:3;subc:30{*0.75~=22}] 92 46
23[pp1:3;pm3:1;subc:11{c(11)=17}]
35[pp1:2;pm3:1;subc:17{c(17)=26}]
53[pp1:1;pm3:5;subc:26{*0.75~=19}] 80 40 20 10
5[pp1:1;pm3:4;subc:2] 8 4 2
1[pp1:1;pm3:2;subc:0]

Attachment: comp3.py
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.