Import dickson.
Import storage.

(* algorithmic content of the axioms *)
tdef S_inj.N = \x\y\z z.
tdef N0_not_S.N = \x\y y. 
tdef equal.reflexive = \x x.
tdef cons.injective.List = \x (\y (y x x)).
tdef nil_not_cons.List = \x x.
tdef length.nil.List = \x x.
tdef length.cons.List = \x\y y.

depend dickson.


compile dickson.
compile LNStor.
compile Spec_dec.
compile N10.total.N.

tdef PN = \n (n "0" "S").
tdef PL = \l (l "\n" \p\c (PN p "," c)).

tdef interact = \l \n (dickson l n (\x (x \r \p (LNStor r \r (PL r (Spec_dec l n r (\t r) (\f (f p)))))))).


tdef pi12 = \x1 \x2 x1.
tdef pi22 = \x1 \x2 x2.
tdef fastmod2aux = \pi (pi pi22 pi12).
tdef fastmod2 = \n (n pi12 fastmod2aux N0.total.N N1.total.N).

tdef pi13 = \x1 \x2 \x3 x1.
tdef pi23 = \x1 \x2 \x3 x2.
tdef pi33 = \x1 \x2 \x3 x3.
tdef fastmod3aux = \pi (pi pi23 pi33 pi13).
tdef fastmod3 = \n (n pi13 fastmod3aux N0.total.N N1.total.N N2.total.N).

tdef pi14 = \x1 \x2 \x3 \x4 x1.
tdef pi24 = \x1 \x2 \x3 \x4 x2.
tdef pi34 = \x1 \x2 \x3 \x4 x3.
tdef pi44 = \x1 \x2 \x3 \x4 x4.
tdef fastmod4aux = \pi (pi pi24 pi34 pi44 pi14).
tdef fastmod4 = \n (n pi14 fastmod4aux N0.total.N N1.total.N N2.total.N N3.total.N).

tdef pi15 = \x1 \x2 \x3 \x4 \x5 x1.
tdef pi25 = \x1 \x2 \x3 \x4 \x5 x2.
tdef pi35 = \x1 \x2 \x3 \x4 \x5 x3.
tdef pi45 = \x1 \x2 \x3 \x4 \x5 x4.
tdef pi55 = \x1 \x2 \x3 \x4 \x5 x5.
tdef fastmod5aux = \pi (pi pi25 pi35 pi45 pi55 pi15).
tdef fastmod5 = \n (n pi15 fastmod5aux N0.total.N N1.total.N N2.total.N N3.total.N N4.total.N).

tdef Ex2 = \nil \cons (cons fastmod2 nil).
tdef Ex3 = \nil \cons (cons fastmod2 (cons fastmod3 nil)).
tdef Ex4 = \nil \cons (cons fastmod2 (cons fastmod3 (cons fastmod4 nil))).
tdef Ex5 = \nil \cons (cons fastmod2 (cons fastmod3 (cons fastmod4 (cons fastmod5 nil)))).

eval interact Ex2 N4.total.N.
(*
(3,2,1,0) (4,3,2,0) (5,4,2,0) 
*)
eval interact Ex2 N5.total.N.
(*
(4,3,2,1,0) (5,4,3,2,0) (6,5,4,2,0) (7,6,4,2,0) 
*)
eval interact Ex3 N4.total.N.
(*
(3,2,1,0) (4,3,2,0) (4,3,1,0) (5,4,3,0) (6,5,4,0) (7,6,4,0) (7,6,3,0) (8,7,6,0) (9,8,6,0) (9,7,6,0) (10,9,6,0) (11,10,6,0) 
*)
eval interact Ex3 N5.total.N.
(*
(4,3,2,1,0) (5,4,3,2,0) (5,4,3,1,0) (6,5,4,3,0) (7,6,5,4,0) (8,7,6,4,0) (8,7,6,3,0) (9,8,7,6,0) (10,9,8,6,0) (10,9,7,6,0) (11,10,9,6,0) (12,11,10,6,0) (13,12,10,6,0) (13,12,9,6,0) (14,13,12,6,0) (15,14,12,6,0) (15,13,12,6,0) (16,15,12,6,0) (17,16,12,6,0)
*)
eval interact Ex4 N4.total.N.
(*
(3,2,1,0) (4,3,2,0) (4,3,1,0) (5,4,3,0) (5,4,2,0) (5,4,1,0) (6,5,4,0) (7,6,4,0) (8,7,6,0) (9,8,6,0) (8,5,4,0) (9,8,4,0) (10,9,4,0) (11,10,9,0) (12,11,10,0) (13,12,10,0) (13,12,9,0) (12,8,4,0) (13,12,4,0) (14,13,12,0) (15,14,12,0) (15,13,12,0) (16,15,12,0) (16,14,12,0) (16,13,12,0) (17,16,12,0) 
*)
eval interact Ex4 N5.total.N.
(*
(4,3,2,1,0) (5,4,3,2,0) (5,4,3,1,0) (6,5,4,3,0) (6,5,4,2,0) (6,5,4,1,0) (7,6,5,4,0) (8,7,6,4,0) (9,8,7,6,0) (10,9,8,6,0) (9,8,5,4,0) (10,9,8,4,0) (11,10,9,4,0) (12,11,10,9,0) (13,12,11,10,0) (14,13,12,10,0) (14,13,12,9,0) (13,12,8,4,0) (14,13,12,4,0) (15,14,13,12,0) (16,15,14,12,0) (16,15,13,12,0) (17,16,15,12,0) (17,16,14,12,0) (17,16,13,12,0) (18,17,16,12,0) (19,18,16,12,0) (20,19,18,12,0) (21,20,18,12,0) (20,17,16,12,0) (21,20,16,12,0) (22,21,16,12,0) (23,22,21,12,0) (24,23,22,12,0) (25,24,22,12,0) (25,24,21,12,0) (24,20,16,12,0) (25,24,16,12,0) (26,25,24,12,0) (27,26,24,12,0) (27,25,24,12,0) (28,27,24,12,0) (28,26,24,12,0) (28,25,24,12,0) (29,28,24,12,0) 
*)
eval interact Ex5 N4.total.N.
(*
(3,2,1,0) (4,3,2,0) (4,3,1,0) (5,4,3,0) (5,4,2,0) (5,4,1,0) (6,5,4,0) (6,5,3,0) (6,5,2,0) (6,5,1,0) (7,6,5,0) (8,7,6,0) (9,8,6,0) (9,8,5,0) (10,9,8,0) (11,10,9,0) (11,10,8,0) (10,7,6,0) (11,10,6,0) (11,10,5,0) (12,11,10,0) (13,12,10,0) (13,12,5,0) (14,13,12,0) (15,14,12,0) (15,13,12,0) (16,15,12,0) (15,11,10,0) (16,15,10,0) (17,16,15,0) (17,16,10,0) (17,16,5,0) (18,17,16,0) (19,18,16,0) (20,19,18,0) (21,20,18,0) (20,17,16,0) (21,20,16,0) (21,20,15,0) (21,20,10,0) (21,20,5,0) (22,21,20,0) (23,22,21,0) (24,23,22,0) (25,24,22,0) (25,24,21,0) (25,24,20,0) (26,25,24,0) (25,23,22,0) (26,25,22,0) (26,25,21,0) (26,25,20,0) (27,26,25,0) (28,27,26,0) (28,27,25,0) (29,28,27,0) (29,28,26,0) (29,28,25,0) (29,28,20,0) (30,29,28,0) (31,30,28,0) (31,30,27,0) (31,30,26,0) (31,30,25,0) (32,31,30,0) (33,32,30,0) (33,32,25,0) (33,32,20,0) (34,33,20,0) (35,34,33,0) (36,35,34,0) (36,35,33,0) (35,32,20,0) (35,31,30,0) (36,35,30,0) (37,36,30,0) (37,36,25,0) (37,36,20,0) (38,37,36,0) (39,38,36,0) (39,37,36,0) (40,39,36,0) (40,38,36,0) (40,37,36,0) (41,40,36,0) (40,35,30,0) (41,40,30,0) (41,40,25,0) (41,40,20,0) (42,41,40,0) (43,42,40,0) (44,43,42,0) (45,44,42,0) (44,41,40,0) (45,44,40,0) (45,43,42,0) (46,45,42,0) (45,41,40,0) (46,45,40,0) (47,46,45,0) (48,47,46,0) (49,48,46,0) (49,48,45,0) (49,48,40,0) (50,49,48,0) (51,50,48,0) (50,47,46,0) (51,50,46,0) (51,50,45,0) (52,51,50,0) (52,51,45,0) (53,52,50,0) (53,52,45,0) (53,52,40,0) 
*)
eval interact Ex5 N5.total.N.
(*
(4,3,2,1,0) (5,4,3,2,0) (5,4,3,1,0) (6,5,4,3,0) (6,5,4,2,0) (6,5,4,1,0) (7,6,5,4,0) (7,6,5,3,0) (7,6,5,2,0) (7,6,5,1,0) (8,7,6,5,0) (9,8,7,6,0) (10,9,8,6,0) (10,9,8,5,0) (11,10,9,8,0) (12,11,10,9,0) (12,11,10,8,0) (11,10,7,6,0) (12,11,10,6,0) (12,11,10,5,0) (13,12,11,10,0) (14,13,12,10,0) (14,13,12,5,0) (15,14,13,12,0) (16,15,14,12,0) (16,15,13,12,0) (17,16,15,12,0) (16,15,11,10,0) (17,16,15,10,0) (18,17,16,15,0) (18,17,16,10,0) (18,17,16,5,0) (19,18,17,16,0) (20,19,18,16,0) (21,20,19,18,0) (22,21,20,18,0) (21,20,17,16,0) (22,21,20,16,0) (22,21,20,15,0) (22,21,20,10,0) (22,21,20,5,0) (23,22,21,20,0) (24,23,22,21,0) (25,24,23,22,0) (26,25,24,22,0) (26,25,24,21,0) (26,25,24,20,0) (27,26,25,24,0) (26,25,23,22,0) (27,26,25,22,0) (27,26,25,21,0) (27,26,25,20,0) (28,27,26,25,0) (29,28,27,26,0) (29,28,27,25,0) (30,29,28,27,0) (30,29,28,26,0) (30,29,28,25,0) (30,29,28,20,0) (31,30,29,28,0) (32,31,30,28,0) (32,31,30,27,0) (32,31,30,26,0) (32,31,30,25,0) (33,32,31,30,0) (34,33,32,30,0) (34,33,32,25,0) (34,33,32,20,0) (35,34,33,20,0) (36,35,34,33,0) (37,36,35,34,0) (37,36,35,33,0) (36,35,32,20,0) (36,35,31,30,0) (37,36,35,30,0) (38,37,36,30,0) (38,37,36,25,0) (38,37,36,20,0) (39,38,37,36,0) (40,39,38,36,0) (40,39,37,36,0) (41,40,39,36,0) (41,40,38,36,0) (41,40,37,36,0) (42,41,40,36,0) (41,40,35,30,0) (42,41,40,30,0) (42,41,40,25,0) (42,41,40,20,0) (43,42,41,40,0) (44,43,42,40,0) (45,44,43,42,0) (46,45,44,42,0) (45,44,41,40,0) (46,45,44,40,0) (46,45,43,42,0) (47,46,45,42,0) (46,45,41,40,0) (47,46,45,40,0) (48,47,46,45,0) (49,48,47,46,0) (50,49,48,46,0) (50,49,48,45,0) (50,49,48,40,0) (51,50,49,48,0) (52,51,50,48,0) (51,50,47,46,0) (52,51,50,46,0) (52,51,50,45,0) (53,52,51,50,0) (53,52,51,45,0) (54,53,52,50,0) (54,53,52,45,0) (54,53,52,40,0) (55,54,52,40,0) (56,55,54,40,0) (57,56,55,54,0) (55,53,52,40,0) (56,55,52,40,0) (56,55,51,45,0) (57,56,55,50,0) (57,56,55,45,0) (58,57,56,50,0) (58,57,56,45,0) (58,57,56,40,0) (59,58,57,40,0) (60,59,58,57,0) (61,60,59,58,0) (62,61,60,58,0) (62,61,60,57,0) (61,60,56,40,0) (61,60,55,45,0) (62,61,60,50,0) (62,61,60,45,0) (62,61,60,40,0) (63,62,61,60,0) (64,63,62,60,0) (64,63,61,60,0) (65,64,63,60,0) (65,64,62,60,0) (65,64,61,60,0) (66,65,64,60,0) (66,65,63,60,0) (66,65,62,60,0) (66,65,61,60,0) (67,66,65,60,0) (68,67,66,60,0) (69,68,66,60,0) (69,68,65,60,0) (70,69,68,60,0) (71,70,69,60,0) (71,70,68,60,0) (70,67,66,60,0) (71,70,66,60,0) (71,70,65,60,0) (72,71,70,60,0) (73,72,70,60,0) (73,72,65,60,0) (74,73,72,60,0) (75,74,72,60,0) (75,73,72,60,0) (76,75,72,60,0) (75,71,70,60,0) (76,75,70,60,0) (77,76,75,60,0) (77,76,70,60,0) (77,76,65,60,0) (78,77,76,60,0) (79,78,76,60,0) (80,79,78,60,0) (81,80,78,60,0) (80,77,76,60,0) (81,80,76,60,0) (81,80,75,60,0) (81,80,70,60,0) (81,80,65,60,0) (82,81,80,60,0) (83,82,81,60,0) (84,83,82,60,0) (85,84,82,60,0) (85,84,81,60,0) (85,84,80,60,0) (86,85,84,60,0) (85,83,82,60,0) (86,85,82,60,0) (86,85,81,60,0) (86,85,80,60,0) (87,86,85,60,0) (88,87,86,60,0) (88,87,85,60,0) (89,88,87,60,0) (89,88,86,60,0) (89,88,85,60,0) (89,88,80,60,0) (90,89,88,60,0) (91,90,88,60,0) (91,90,87,60,0) (91,90,86,60,0) (91,90,85,60,0) (92,91,90,60,0) (93,92,90,60,0) (93,92,85,60,0) (93,92,80,60,0) (94,93,80,60,0) (95,94,93,60,0) (96,95,94,60,0) (96,95,93,60,0) (95,92,80,60,0) (95,91,90,60,0) (96,95,90,60,0) (97,96,90,60,0) (97,96,85,60,0) (97,96,80,60,0) (98,97,96,60,0) (99,98,96,60,0) (99,97,96,60,0) (100,99,96,60,0) (100,98,96,60,0) (100,97,96,60,0) (101,100,96,60,0) (100,95,90,60,0) (101,100,90,60,0) (101,100,85,60,0) (101,100,80,60,0) (102,101,100,60,0) (103,102,100,60,0) (104,103,102,60,0) (105,104,102,60,0) (104,101,100,60,0) (105,104,100,60,0) (105,103,102,60,0) (106,105,102,60,0) (105,101,100,60,0) (106,105,100,60,0) (107,106,105,60,0) (108,107,106,60,0) (109,108,106,60,0) (109,108,105,60,0) (109,108,100,60,0) (110,109,108,60,0) (111,110,108,60,0) (110,107,106,60,0) (111,110,106,60,0) (111,110,105,60,0) (112,111,110,60,0) (112,111,105,60,0) (113,112,110,60,0) (113,112,105,60,0) (113,112,100,60,0) 
*)