equal
deleted
inserted
replaced
56 TR7 "F : (HasTok i) leadsTo (HasTok (next i))" |
56 TR7 "F : (HasTok i) leadsTo (HasTok (next i))" |
57 |
57 |
58 defines |
58 defines |
59 nodeOrder_def |
59 nodeOrder_def |
60 "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int |
60 "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int |
61 (lessThan N Times lessThan N)" |
61 (lessThan N <*> lessThan N)" |
62 |
62 |
63 next_def |
63 next_def |
64 "next i == (Suc i) mod N" |
64 "next i == (Suc i) mod N" |
65 |
65 |
66 end |
66 end |