multiset-fib.modal

<> (tally ?v (Bag ?l)) ((Bag tallying| tallying> ?v ?l)) <> (tallying> ?v ()) (<tallying ((Entry ?v 1) ())) <> (tallying> ?v ((Entry ?v ?c) ?r)) (<tallying ((Entry ?v ?((?: ?0 ?1) ?:) + ?c 1) ?r)) <> (tallying> ?v (?e ?r)) ((?e tallying> ?v ?r)) <> ((Bag tallying| <tallying ?l)) ((Bag ?l)) <> ((?e <tallying ?p)) (<tallying (?e ?p)) <> (tally all ()) () <> (tally all (?i ?r) (Bag ?l)) (tally all ?r tally ?i (Bag ?l)) <> (find ?v (Bag ?l)) ((Bag find| find> ?v ?l)) <> (find> ?v ((Entry ?v ?c) ?r)) (<found #yes ((Entry ?v ?c) ?r)) <> (find> ?v ()) (<found #no ()) <> (find> ?v (?e ?r)) ((?e find> ?v ?r)) <> ((Bag find| <found ?a ?l)) (?a (Bag ?l)) <> ((?e <found ?a ?p)) (<found ?a (?e ?p)) <> (has all ()) (#yes) <> (has all (?i ?r)) (?r has all| find ?i) <> (?r has all| #yes) (has all ?r) <> (?r has all| #no) (#no) <> (remove ?i (Bag ?r)) ((Bag remove| remove> ?i ?r)) <> (remove> ?i ()) (<remove ()) <> (remove> ?i ((Entry ?i ?c) ?r)) (removing ((Entry ?i ?((?: ?0 ?1) ?:) - ?c 1) ?r)) <> (remove> ?i (?e ?r)) ((?e remove> ?i ?r)) <> (removing ((Entry ?i 0) ?r)) (<remove ?r) <> (removing ((Entry ?i ?c) ?r)) (<remove ((Entry ?i ?c) ?r)) <> ((Bag remove| <remove ?l)) ((Bag ?l)) <> ((?e <remove ?p)) (<remove (?e ?p)) <> (remove all ()) () <> (remove all (?i ?r) (Bag ?l)) (remove all ?r remove ?i (Bag ?l)) <> (:) (takes>) <> (takes> >) (g>) <> (g> ;) ((Recipe () ())) <> (takes> ?i) (take ?i takes>) <> (g> ?i) (give ?i g>) <> (give ?i (Recipe ?n ?g)) ((Recipe ?n (?i ?g))) <> (take ?i (Recipe ?n ?g)) ((Recipe (?i ?n) ?g)) <> ((Recipe () ?g)) () <> (recipes) (recipes>) <> (recipes> (Bag ?l)) (<ready (Bag ?l)) <> (recipes> (Recipe ?n ?g)) ((Recipe ?n ?g) recipes>) <> ((Recipe ?n ?g) <ready) (<ready (Recipe ?n ?g)) <> (<ready) (rewrite) <> (bag {) (bag) <> (bag }) ((Bag ())) <> (bag ?i) (tally ?i bag) <> (rewrite (Recipe ?n ?g)) (rewrite| (Recipe ?n ?g) test> ?n) <> (test> ?n (Bag ?l)) (test| ?n has all ?n (Bag ?l)) <> (test> ?n ?r) (?r test> ?n) <> (test| ?n #yes) (match| #yes remove all ?n) <> (test| ?n #no) (<match #no) <> (match| #yes (Bag ?l)) (<match #yes (Bag ?l)) <> (rewrite| <match #yes (Recipe ?n ?g)) (rewrite| (Recipe ?n ?g) update> ?g) <> (rewrite| <match #no) (rewrite>) <> (?r <match ?a) (<match ?a ?r) <> (update> ?g (Bag ?l)) (update| tally all ?g (Bag ?l)) <> (update> ?g ?r) (?r update> ?g) <> (update| (Bag ?l)) (<update (Bag ?l)) <> (rewrite| <update) (<rewrite) <> (?r <update) (<update ?r) <> (?r <rewrite) (<rewrite ?r) <> (<rewrite) (rewrite) <> (rewrite (Bag ?l)) (done (Bag ?l)) <> (rewrite> ?r) (?r rewrite) <> (?r done) (done) recipes : fib n > fib.shift ; : fib.shift n1 > fib.shift N2 ; : fib.shift n2 > fib.shift N1 N2 ; : fib.shift > fib.move ; : fib.move N1 > fib.move n1 ; : fib.move N2 > fib.move n2 ; : fib.move > fib ; : n1 > ; : fib > ; bag { n n n n n n1 n2 fib }

1	<> (tally ?v (Bag ?l)) ((Bag tallying\| tallying> ?v ?l))
2
3	<> (tallying> ?v ())
4	(<tallying ((Entry ?v 1) ()))
5
6	<> (tallying> ?v ((Entry ?v ?c) ?r))
7	(<tallying ((Entry ?v ?((?: ?0 ?1) ?:) + ?c 1) ?r))
8
9	<> (tallying> ?v (?e ?r))
10	((?e tallying> ?v ?r))
11
12	<> ((Bag tallying\| <tallying ?l)) ((Bag ?l))
13	<> ((?e <tallying ?p)) (<tallying (?e ?p))
14
15	<> (tally all ()) ()
16	<> (tally all (?i ?r) (Bag ?l)) (tally all ?r tally ?i (Bag ?l))
17
18
19
20	<> (find ?v (Bag ?l)) ((Bag find\| find> ?v ?l))
21
22	<> (find> ?v ((Entry ?v ?c) ?r))
23	(<found #yes ((Entry ?v ?c) ?r))
24	<> (find> ?v ()) (<found #no ())
25
26	<> (find> ?v (?e ?r)) ((?e find> ?v ?r))
27
28	<> ((Bag find\| <found ?a ?l)) (?a (Bag ?l))
29	<> ((?e <found ?a ?p)) (<found ?a (?e ?p))
30
31
32
33	<> (has all ()) (#yes)
34	<> (has all (?i ?r)) (?r has all\| find ?i)
35	<> (?r has all\| #yes) (has all ?r)
36	<> (?r has all\| #no) (#no)
37
38
39
40	<> (remove ?i (Bag ?r)) ((Bag remove\| remove> ?i ?r))
41
42	<> (remove> ?i ()) (<remove ())
43	<> (remove> ?i ((Entry ?i ?c) ?r)) (removing ((Entry ?i ?((?: ?0 ?1) ?:) - ?c 1) ?r))
44	<> (remove> ?i (?e ?r)) ((?e remove> ?i ?r))
45
46	<> (removing ((Entry ?i 0) ?r)) (<remove ?r)
47	<> (removing ((Entry ?i ?c) ?r)) (<remove ((Entry ?i ?c) ?r))
48
49	<> ((Bag remove\| <remove ?l)) ((Bag ?l))
50	<> ((?e <remove ?p)) (<remove (?e ?p))
51
52	<> (remove all ()) ()
53	<> (remove all (?i ?r) (Bag ?l)) (remove all ?r remove ?i (Bag ?l))
54
55
56	<> (:) (takes>)
57	<> (takes> >) (g>)
58	<> (g> ;) ((Recipe () ()))
59
60	<> (takes> ?i) (take ?i takes>)
61	<> (g> ?i) (give ?i g>)
62
63	<> (give ?i (Recipe ?n ?g)) ((Recipe ?n (?i ?g)))
64	<> (take ?i (Recipe ?n ?g)) ((Recipe (?i ?n) ?g))
65
66	<> ((Recipe () ?g)) ()
67
68	<> (recipes) (recipes>)
69
70	<> (recipes> (Bag ?l)) (<ready (Bag ?l))
71	<> (recipes> (Recipe ?n ?g)) ((Recipe ?n ?g) recipes>)
72
73	<> ((Recipe ?n ?g) <ready) (<ready (Recipe ?n ?g))
74	<> (<ready) (rewrite)
75
76	<> (bag {) (bag)
77	<> (bag }) ((Bag ()))
78	<> (bag ?i) (tally ?i bag)
79
80
81	<> (rewrite (Recipe ?n ?g)) (rewrite\| (Recipe ?n ?g) test> ?n)
82
83	<> (test> ?n (Bag ?l)) (test\| ?n has all ?n (Bag ?l))
84	<> (test> ?n ?r) (?r test> ?n)
85
86	<> (test\| ?n #yes) (match\| #yes remove all ?n)
87	<> (test\| ?n #no) (<match #no)
88
89	<> (match\| #yes (Bag ?l)) (<match #yes (Bag ?l))
90
91	<> (rewrite\| <match #yes (Recipe ?n ?g)) (rewrite\| (Recipe ?n ?g) update> ?g)
92	<> (rewrite\| <match #no) (rewrite>)
93	<> (?r <match ?a) (<match ?a ?r)
94
95	<> (update> ?g (Bag ?l)) (update\| tally all ?g (Bag ?l))
96	<> (update> ?g ?r) (?r update> ?g)
97
98	<> (update\| (Bag ?l)) (<update (Bag ?l))
99
100	<> (rewrite\| <update) (<rewrite)
101	<> (?r <update) (<update ?r)
102
103	<> (?r <rewrite) (<rewrite ?r)
104	<> (<rewrite) (rewrite)
105
106	<> (rewrite (Bag ?l)) (done (Bag ?l))
107	<> (rewrite> ?r) (?r rewrite)
108
109	<> (?r done) (done)
110
111
112	recipes
113	: fib n > fib.shift ;
114
115	: fib.shift n1 > fib.shift N2 ;
116	: fib.shift n2 > fib.shift N1 N2 ;
117	: fib.shift > fib.move ;
118
119	: fib.move N1 > fib.move n1 ;
120	: fib.move N2 > fib.move n2 ;
121	: fib.move > fib ;
122
123	: n1 > ;
124	: fib > ;
125
126
127	bag { n n n n n n1 n2 fib }