1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
set show timing off .
set show advisories off .
select NAT .
red s 0 + s s 0 .
red s 0 + s 0 .
red _+_(s 0, N:Nat, s 0) .
red sd(s s 0, s s s 0) .
red sd(s_^3(0), s_^10(0)) .
red sd(s_^10(0), s_^4(0)) .
red s 0 * s s 0 .
red s 0 * s 0 .
red s_^10(0) quo s_^4(0) .
red s_^10(0) rem s_^4(0) .
red s_^10(0) ^ s_^4(0) .
red modExp(s_^37(0), s_^1000000000000002(0), s_^100(0)) .
red modExp(s_^37(0), s_^1000000000000002(0), s_^1000003(0)) .
red modExp(s_^100200300400(0), s_^1000000000000002(0), s_^1000003(0)) .
red gcd(gcd(s_^120(0), X:Nat), gcd(s_^140(0), Y:Nat)) .
red gcd(s_^124(0), s_^346(0), s_^768(0)) .
red lcm(lcm(s_^120(0), X:Nat), lcm(s_^140(0), Y:Nat)) .
red lcm(s_^124(0), s_^346(0), s_^768(0)) .
red s 0 xor s s 0 .
red s 0 xor s 0 .
red s 0 & s s 0 .
red s 0 & s 0 .
red s 0 | s s 0 .
red s 0 | s 0 .
red s 0 << s s s 0 .
red s_^128(0) >> s s s 0 .
red s 0 < s s 0 .
red s 0 < s 0 .
red s 0 <= s s 0 .
red s 0 <= s 0 .
red s 0 > s s 0 .
red s 0 > s 0 .
red s 0 >= s s 0 .
red s 0 >= s 0 .
red s_^3(0) divides s_^10(0) .
red s_^3(0) divides s_^9(0) .
fmod FACT is
inc NAT .
op _! : Nat -> NzNat .
var N : Nat .
eq 0 ! = s 0 .
eq (s N) ! = s N * N ! .
endfm
red s_^100(0) ! .
red s_^1000(0) ! .
fmod MOD3 is
inc NAT .
eq s_^3(0) = 0 .
endfm
red s_^4(0) .
fmod FACT' is
inc NAT .
op _! : Nat -> NzNat .
var N : Nat .
eq 0 ! = 1 .
eq (s N) ! = (s N) * N ! .
endfm
red 100 ! .
red 1000 ! .
fmod MOD3' is
inc NAT .
eq 3 = 0 .
endfm
red 4445 .
select NAT .
red 8888888888888888888888888888888888888888888888888888888 .
red s_^123456789(s_^123456789(0)) .
select NAT .
set print graph on .
red 123 .
set trace on .
set trace whole on .
red 4 + 5 .
set trace off .
set print graph off .
|
