Data.lean`

262 declarations, 0 contain sorry, 0 declared as axioms

Untrusted literal certificate data. The subsequent Check modules check the linear identities. Hadamard interpretation is separate.

def OAI.MUB6.Certificate.PairData.row0 line 10
Source comment
Selected source equation 0 in the original pair table.
```
def row0 : Integer.Sparse (Fin 271) := [(0, 9), (1, 170), (2, -25), (3, -80), (4, -160), (12, -40)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row1 line 13
Source comment
Selected source equation 1 in the original pair table.
```
def row1 : Integer.Sparse (Fin 271) := [(0, -1), (1, -4), (5, -8), (6, 1), (27, 12)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row2 line 16
Source comment
Selected source equation 2 in the original pair table.
```
def row2 : Integer.Sparse (Fin 271) := [(0, -1), (1, 18), (2, -8), (3, -64), (4, -32), (5, 3), (7, -16), (8, -8), (12, -24), (23, 12), (24, 24)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row3 line 19
Source comment
Selected source equation 3 in the original pair table.
```
def row3 : Integer.Sparse (Fin 271) := [(0, -9), (1, 205), (2, -110), (3, -160), (4, -160), (5, 30), (7, -40), (8, -200), (24, 120), (29, 240)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row4 line 22
Source comment
Selected source equation 4 in the original pair table.
```
def row4 : Integer.Sparse (Fin 271) := [(0, -4), (1, 95), (2, -25), (3, -320), (4, -160), (12, -160), (13, -80)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row5 line 25
Source comment
Selected source equation 5 in the original pair table.
```
def row5 : Integer.Sparse (Fin 271) := [(0, -11), (1, 250), (2, -45), (3, -800), (4, -480), (12, -320), (25, 120), (26, -160)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row6 line 28
Source comment
Selected source equation 6 in the original pair table.
```
def row6 : Integer.Sparse (Fin 271) := [(0, -9), (1, 315), (2, -70), (3, -480), (4, -400), (12, -80), (26, -80), (30, 240)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row7 line 31
Source comment
Selected source equation 7 in the original pair table.
```
def row7 : Integer.Sparse (Fin 271) := [(0, 1), (1, -8), (2, 4), (14, 18), (17, 72), (23, -48), (25, -96), (27, 9), (29, -24), (30, -96)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row8 line 34

Source comment

Selected source equation 8 in the original pair table.

def row8 : Integer.Sparse (Fin 271) := [(0, 149), (1, -1760), (2, 285), (3, 2080), (4, 2880), (12, 800), (15, 720), (20, 1440), (23, -240), (24, -720), (25, -480), (27, 180), (29, -480), (30, -960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row9 line 37

Source comment

Selected source equation 9 in the original pair table.

def row9 : Integer.Sparse (Fin 271) := [(0, -11), (1, -150), (2, 80), (3, 640), (4, 320), (12, 240), (16, 180), (17, 360), (23, -240), (27, 45), (29, -120)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row10 line 40
Source comment
Selected source equation 10 in the original pair table.
```
def row10 : Integer.Sparse (Fin 271) := [(0, 11), (1, -890), (2, 45), (3, 1120), (4, 1080), (12, 440), (18, 360), (22, 720)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row11 line 43

Source comment

Selected source equation 11 in the original pair table.

def row11 : Integer.Sparse (Fin 271) := [(0, 12), (1, -121), (2, 33), (3, 320), (4, 224), (12, 192), (15, 144), (17, 72), (23, -72), (24, -48), (25, -144), (27, 18), (29, -24), (30, -144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row12 line 46

Source comment

Selected source equation 12 in the original pair table.

def row12 : Integer.Sparse (Fin 271) := [(0, 3), (1, -65), (2, 11), (3, 80), (4, 80), (12, 20), (17, 36), (19, 36), (20, 36), (22, 36), (24, -60), (27, 9), (29, -12), (30, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row13 line 49
Source comment
Selected source equation 13 in the original pair table.
```
def row13 : Integer.Sparse (Fin 271) := [(0, 93), (1, -1715), (2, 210), (3, 2880), (4, 2400), (12, 1520), (21, 720), (22, 720), (30, -480)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row14 line 52
Source comment
Selected source equation 14 in the original pair table.
```
def row14 : Integer.Sparse (Fin 271) := [(0, 16), (1, -315), (2, 65), (3, 960), (4, 600), (12, 360), (18, 360), (25, -240), (30, -240)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row15 line 55
Source comment
Selected source equation 16 in the original pair table.
```
def row15 : Integer.Sparse (Fin 271) := [(0, -69), (1, -470), (2, 110), (3, 160), (4, 160), (12, 160), (17, 180), (23, -60), (27, 45), (28, 360), (29, -300)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row16 line 58

Source comment

Selected source equation 17 in the original pair table.

def row16 : Integer.Sparse (Fin 271) := [(0, -11), (1, 220), (2, -250), (3, -1200), (4, -240), (5, 260), (6, -15), (7, -480), (8, -480), (12, -480), (13, -320), (34, -160), (50, 720), (51, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row17 line 61

Source comment

Selected source equation 18 in the original pair table.

def row17 : Integer.Sparse (Fin 271) := [(0, -32), (1, 615), (2, -60), (3, -2160), (4, -960), (5, 60), (6, -15), (12, -240), (13, -160), (26, -960), (34, -240), (54, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row18 line 64

Source comment

Selected source equation 19 in the original pair table.

def row18 : Integer.Sparse (Fin 271) := [(0, -7), (1, 125), (2, -70), (3, -480), (4, -160), (5, 160), (6, -20), (7, -80), (8, -160), (26, -160), (34, -80), (51, -160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row19 line 67

Source comment

Selected source equation 20 in the original pair table.

def row19 : Integer.Sparse (Fin 271) := [(0, -2), (1, 55), (2, -11), (3, -304), (4, -64), (5, 52), (6, -8), (7, -16), (8, -32), (12, -64), (13, -208), (26, -64), (34, -80), (51, -64), (53, 48), (55, 96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row20 line 70
Source comment
Selected source equation 21 in the original pair table.
```
def row20 : Integer.Sparse (Fin 271) := [(0, -11), (1, 215), (2, -95), (3, -720), (4, -240), (5, 160), (6, -15), (7, -240), (8, -240), (26, -240), (34, -80)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row21 line 73
Source comment
Selected source equation 22 in the original pair table.
```
def row21 : Integer.Sparse (Fin 271) := [(0, 1), (1, 5), (3, -400), (5, 10), (7, -160), (12, -240), (13, -240), (23, 360), (25, 360), (34, -80), (53, 240)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row22 line 76
Source comment
Selected source equation 23 in the original pair table.
```
def row22 : Integer.Sparse (Fin 271) := [(0, -7), (1, 180), (2, -15), (3, -720), (12, -360), (13, -960), (31, -80)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row23 line 79
Source comment
Selected source equation 24 in the original pair table.
```
def row23 : Integer.Sparse (Fin 271) := [(0, -7), (1, 145), (2, -30), (3, -680), (4, -240), (12, -120), (13, -160), (26, -280), (32, 120), (33, -80)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row24 line 82
Source comment
Selected source equation 25 in the original pair table.
```
def row24 : Integer.Sparse (Fin 271) := [(0, -19), (1, 300), (2, -75), (3, -640), (4, -480), (12, -200), (25, 240), (26, -80), (30, 480), (32, 240)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row25 line 85

Source comment

Selected source equation 26 in the original pair table.

def row25 : Integer.Sparse (Fin 271) := [(0, 157), (1, -2040), (2, 585), (3, 5280), (4, 3520), (12, 2240), (13, 560), (25, -1200), (30, -2880), (32, -960), (49, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row26 line 88

Source comment

Selected source equation 27 in the original pair table.

def row26 : Integer.Sparse (Fin 271) := [(0, 59), (1, -575), (2, 320), (3, 1040), (4, 480), (5, -80), (7, 80), (8, 320), (12, 480), (23, -240), (25, -240), (27, 180), (29, -480), (30, -480), (32, -480), (44, 1440), (50, -480), (53, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row27 line 91

Source comment

Selected source equation 28 in the original pair table.

def row27 : Integer.Sparse (Fin 271) := [(0, 29), (1, -334), (2, 99), (3, 896), (4, 512), (12, 352), (13, 32), (25, -96), (26, 112), (30, -336), (32, -192), (42, 144), (44, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row28 line 94

Source comment

Selected source equation 29 in the original pair table.

def row28 : Integer.Sparse (Fin 271) := [(0, 128), (1, -1575), (2, 405), (3, 4480), (4, 2960), (12, 1360), (25, -960), (26, 960), (30, -1680), (42, 720), (43, 720), (44, 720), (45, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row29 line 97

Source comment

Selected source equation 30 in the original pair table.

def row29 : Integer.Sparse (Fin 271) := [(0, 58), (1, -605), (2, 235), (3, 1280), (4, 920), (5, -30), (7, 40), (8, 80), (12, 560), (23, -240), (24, -720), (25, -600), (27, 300), (29, -480), (30, -1200), (32, -480), (47, 360), (48, 720), (50, -360), (54, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row30 line 100

Source comment

Selected source equation 31 in the original pair table.

def row30 : Integer.Sparse (Fin 271) := [(0, 141), (1, -1765), (2, 580), (3, 3600), (4, 2560), (5, -60), (7, 80), (8, 160), (12, 1440), (13, 320), (23, -480), (24, -1440), (27, 600), (29, -960), (30, -1920), (46, 720), (48, 1440), (50, -720), (54, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row31 line 103

Source comment

Selected source equation 32 in the original pair table.

def row31 : Integer.Sparse (Fin 271) := [(0, 109), (1, -1300), (2, 565), (3, 2880), (4, 1760), (5, -120), (7, 160), (8, 320), (12, 800), (23, -480), (24, -1440), (26, 400), (27, 600), (29, -960), (30, -1200), (42, 720), (54, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row32 line 106

Source comment

Selected source equation 33 in the original pair table.

def row32 : Integer.Sparse (Fin 271) := [(0, 56), (1, -675), (2, 305), (3, 1760), (4, 1120), (5, -80), (7, 160), (8, 240), (12, 440), (24, -480), (26, 160), (27, 180), (29, -240), (30, -720), (44, 360), (45, 360), (50, -480), (55, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row33 line 109

Source comment

Selected source equation 34 in the original pair table.

def row33 : Integer.Sparse (Fin 271) := [(0, 67), (1, -1010), (2, 185), (3, 3200), (4, 960), (5, -60), (7, 80), (8, 160), (12, 1040), (13, 1200), (25, -960), (26, 640), (30, -960), (32, -960), (37, 720), (38, 1440), (53, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row34 line 112

Source comment

Selected source equation 35 in the original pair table.

def row34 : Integer.Sparse (Fin 271) := [(0, 8), (1, -151), (2, 109), (3, 624), (4, 192), (5, -44), (7, 48), (8, 160), (12, 96), (23, -48), (25, -96), (26, 128), (27, 36), (29, -96), (30, -192), (32, -384), (35, 144), (38, 288), (39, 288), (50, -192), (53, -240), (54, -144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row35 line 115

Source comment

Selected source equation 36 in the original pair table.

def row35 : Integer.Sparse (Fin 271) := [(0, 19), (1, -288), (2, 91), (3, 928), (4, 512), (5, -12), (7, 16), (8, 32), (12, 48), (13, 32), (26, 368), (36, 144), (39, 288), (55, -144), (56, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row36 line 118

Source comment

Selected source equation 37 in the original pair table.

def row36 : Integer.Sparse (Fin 271) := [(0, 37), (1, -580), (2, 255), (3, 1920), (4, 320), (5, -80), (7, 80), (8, 320), (12, 720), (13, 880), (23, -120), (26, 160), (27, 90), (29, -240), (37, 360), (39, 720), (50, -480), (53, -240), (54, -360)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row37 line 121

Source comment

Selected source equation 38 in the original pair table.

def row37 : Integer.Sparse (Fin 271) := [(0, 16), (1, -255), (2, 93), (3, 896), (4, 304), (12, 384), (13, 448), (26, 112), (30, -192), (32, -192), (40, 144), (41, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row38 line 124
Source comment
Selected source equation 39 in the original pair table.
```
def row38 : Integer.Sparse (Fin 271) := [(0, 17), (1, -309), (2, 76), (3, 1008), (4, 480), (26, 528), (52, 144), (56, 144)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row39 line 127

Source comment

Selected source equation 40 in the original pair table.

def row39 : Integer.Sparse (Fin 271) := [(0, 9), (1, -179), (2, 82), (3, 720), (4, 288), (5, -32), (7, 64), (8, 96), (12, 160), (13, 128), (24, -96), (26, 176), (27, 36), (29, -48), (30, -96), (32, -192), (36, 144), (38, 144), (39, 144), (41, 144), (50, -192), (54, -144), (55, -96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row40 line 130

Source comment

Selected source equation 41 in the original pair table.

def row40 : Integer.Sparse (Fin 271) := [(0, 1), (1, -145), (2, 70), (3, 1200), (4, 400), (5, -10), (7, 80), (12, 720), (14, 360), (15, 1440), (23, -840), (24, -480), (25, -840), (27, 120), (32, -480), (35, 720), (47, 720), (50, -240), (53, -240), (54, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row41 line 133

Source comment

Selected source equation 42 in the original pair table.

def row41 : Integer.Sparse (Fin 271) := [(0, 83), (1, -1010), (2, 145), (3, 5280), (4, 1920), (12, 1760), (13, 720), (15, 1440), (16, 720), (18, 2880), (23, -480), (24, -480), (25, -720), (27, 60), (37, 1440), (49, 720), (54, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row42 line 136

Source comment

Selected source equation 43 in the original pair table.

def row42 : Integer.Sparse (Fin 271) := [(0, 88), (1, -1245), (2, 255), (3, 4080), (4, 1760), (5, -20), (7, 80), (8, 80), (12, 880), (15, 720), (18, 720), (19, 1440), (21, 1440), (23, -240), (24, -1440), (25, -240), (26, 480), (27, 180), (30, -960), (36, 1440), (46, 720), (47, 720), (50, -480), (55, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row43 line 139

Source comment

Selected source equation 44 in the original pair table.

def row43 : Integer.Sparse (Fin 271) := [(0, 79), (1, -810), (2, 195), (3, 1040), (4, 1320), (5, -20), (7, 80), (8, 120), (12, 160), (17, 360), (20, 720), (23, -120), (24, -600), (25, -360), (26, 80), (27, 90), (29, -360), (30, -720), (43, 720), (44, 720), (47, 360), (50, -120)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row44 line 142
Source comment
Selected source equation 45 in the original pair table.
```
def row44 : Integer.Sparse (Fin 271) := [(0, 1), (1, -25), (2, -25), (9, -100), (57, 5)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse
def OAI.MUB6.Certificate.PairData.row45 line 145
Source comment
Selected source equation 46 in the original pair table.
```
def row45 : Integer.Sparse (Fin 271) := [(0, 1), (1, -24), (2, 36), (5, -120), (6, 15), (9, -16), (27, 180), (66, 240)]
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row46 line 148

Source comment

Selected source equation 47 in the original pair table.

def row46 : Integer.Sparse (Fin 271) := [(0, 1), (1, -25), (2, -150), (3, -240), (5, 320), (6, -30), (7, -480), (8, -480), (9, 40), (34, -160), (67, -240), (68, -80), (69, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row47 line 151

Source comment

Selected source equation 48 in the original pair table.

def row47 : Integer.Sparse (Fin 271) := [(0, -1), (1, 55), (2, -10), (3, -480), (5, -20), (7, -480), (9, 20), (12, -320), (13, -160), (23, 720), (34, -320), (67, -320), (68, -160), (111, 720), (112, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row48 line 154

Source comment

Selected source equation 49 in the original pair table.

def row48 : Integer.Sparse (Fin 271) := [(0, -9), (1, 135), (2, -160), (3, -1280), (4, -480), (5, 260), (6, -30), (7, -720), (8, -240), (9, 20), (24, 720), (26, -480), (34, -640), (51, -480), (67, -240), (68, -160), (69, -80), (113, 720), (131, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row49 line 157

Source comment

Selected source equation 50 in the original pair table.

def row49 : Integer.Sparse (Fin 271) := [(0, 3), (1, 105), (2, -90), (3, -1440), (5, 210), (6, -30), (7, -480), (9, 10), (12, -600), (13, -1240), (23, 360), (34, -720), (51, -480), (53, 720), (67, -120), (68, -120), (112, 360), (130, 240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row50 line 160

Source comment

Selected source equation 51 in the original pair table.

def row50 : Integer.Sparse (Fin 271) := [(0, -4), (1, 45), (2, -230), (3, -640), (4, -160), (5, 280), (6, -15), (7, -480), (8, -480), (9, 20), (24, 480), (27, -60), (50, 480), (51, -160), (67, -160), (69, -320), (111, 240), (113, 960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row51 line 163

Source comment

Selected source equation 52 in the original pair table.

def row51 : Integer.Sparse (Fin 271) := [(0, -14), (1, 65), (2, -250), (3, -320), (5, 440), (6, -45), (7, -160), (8, -800), (9, 20), (27, -60), (29, 480), (51, -160), (67, -80), (69, -400), (113, 240), (146, 960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row52 line 166

Source comment

Selected source equation 53 in the original pair table.

def row52 : Integer.Sparse (Fin 271) := [(0, -2), (1, 95), (2, -60), (3, -880), (4, -320), (5, 460), (6, -65), (7, -160), (8, -480), (9, 20), (13, -400), (24, 480), (26, -320), (34, -400), (51, -320), (54, 240), (55, 960), (67, -80), (68, -80), (69, -320), (112, 240), (131, 960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row53 line 169

Source comment

Selected source equation 54 in the original pair table.

def row53 : Integer.Sparse (Fin 271) := [(0, -1), (1, 35), (2, -140), (3, -480), (5, 265), (6, -15), (7, -600), (8, -480), (10, 180), (12, -120), (13, -160), (34, -320), (80, -60)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row54 line 172

Source comment

Selected source equation 55 in the original pair table.

def row54 : Integer.Sparse (Fin 271) := [(0, -1), (1, 10), (2, -205), (3, -1200), (4, -240), (5, 680), (6, -90), (7, -480), (8, -480), (11, -240), (26, -480), (34, -1120), (51, -1200), (143, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row55 line 175

Source comment

Selected source equation 56 in the original pair table.

def row55 : Integer.Sparse (Fin 271) := [(0, 1), (1, -30), (2, -50), (3, -160), (5, 90), (6, -15), (7, -40), (8, -80), (12, -20), (13, -160), (34, -160), (51, -320), (80, -120), (115, -160), (132, 60), (133, 240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row56 line 178

Source comment

Selected source equation 57 in the original pair table.

def row56 : Integer.Sparse (Fin 271) := [(0, -1), (1, -10), (2, -5), (3, -480), (5, 10), (7, -240), (10, 360), (12, -240), (13, -640), (34, -320), (80, -120), (114, 360), (115, -120)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row57 line 181

Source comment

Selected source equation 58 in the original pair table.

def row57 : Integer.Sparse (Fin 271) := [(0, -9), (1, 525), (2, 90), (3, -3360), (4, -1200), (5, 140), (6, -30), (7, -240), (11, -240), (12, -960), (13, -1680), (25, 720), (26, -1440), (34, -1520), (51, -240), (53, 2160), (55, 1440), (142, 480), (143, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row58 line 184

Source comment

Selected source equation 59 in the original pair table.

def row58 : Integer.Sparse (Fin 271) := [(0, -19), (1, 270), (2, -105), (3, -1360), (4, -560), (5, 240), (6, -40), (11, -80), (26, -640), (27, -120), (30, 480), (34, -480), (51, -400), (54, 480), (143, 240), (147, 480), (148, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row59 line 187

Source comment

Selected source equation 60 in the original pair table.

def row59 : Integer.Sparse (Fin 271) := [(1, 35), (2, -13), (3, -400), (4, -64), (5, 44), (6, -8), (7, -48), (12, -144), (13, -368), (26, -64), (34, -208), (51, -128), (53, 144), (55, 96), (80, -64), (115, -64), (132, 48), (133, 96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row60 line 190

Source comment

Selected source equation 64 in the original pair table.

def row60 : Integer.Sparse (Fin 271) := [(0, 7), (1, -140), (2, -465), (3, -1680), (5, 1240), (6, -160), (7, -960), (8, -960), (12, -240), (13, -1120), (34, -1520), (51, -1920), (58, 720), (59, -320), (115, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row61 line 193

Source comment

Selected source equation 65 in the original pair table.

def row61 : Integer.Sparse (Fin 271) := [(0, 1), (1, -5), (2, -120), (3, -480), (4, -80), (5, 240), (6, -20), (7, -480), (8, -320), (26, -160), (34, -400), (51, -160), (65, -80), (79, 240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row62 line 196

Source comment

Selected source equation 66 in the original pair table.

def row62 : Integer.Sparse (Fin 271) := [(0, 12), (1, 50), (2, -15), (3, -1760), (5, 20), (6, -5), (12, -720), (13, -2000), (26, -560), (31, -160), (32, 720), (33, -480), (34, -240), (54, 720), (59, -160), (60, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row63 line 199

Source comment

Selected source equation 67 in the original pair table.

def row63 : Integer.Sparse (Fin 271) := [(0, 2), (1, 6), (2, -5), (3, -256), (5, 8), (6, -1), (12, -96), (13, -224), (25, 48), (26, -64), (32, 192), (33, -32), (34, -32), (51, -32), (54, 96), (62, 48), (63, 96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row64 line 202

Source comment

Selected source equation 68 in the original pair table.

def row64 : Integer.Sparse (Fin 271) := [(0, 8), (1, 40), (2, -15), (3, -1120), (5, 60), (6, -15), (7, -160), (12, -320), (13, -800), (23, 240), (26, -480), (32, 480), (33, -320), (34, -480), (53, 480), (54, 480), (62, 240), (64, 480), (65, -160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row65 line 205

Source comment

Selected source equation 70 in the original pair table.

def row65 : Integer.Sparse (Fin 271) := [(0, 9), (1, -5), (2, -65), (3, -1440), (5, 60), (6, -5), (12, -720), (13, -2640), (26, -240), (31, -320), (33, -480), (34, -240), (51, -480), (58, 720), (59, -400), (60, 720), (115, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row66 line 208

Source comment

Selected source equation 71 in the original pair table.

def row66 : Integer.Sparse (Fin 271) := [(0, 1), (2, -7), (3, -144), (5, 14), (6, -2), (7, -24), (12, -48), (13, -160), (26, -24), (31, -16), (32, 72), (34, -72), (51, -48), (53, 72), (59, -16), (61, 48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row67 line 211

Source comment

Selected source equation 72 in the original pair table.

def row67 : Integer.Sparse (Fin 271) := [(0, -16), (1, 485), (2, -240), (3, -3440), (4, -1280), (5, 120), (6, -5), (7, -480), (8, -160), (12, -320), (13, -320), (25, 240), (26, -1600), (30, 480), (32, 960), (33, -400), (34, -560), (50, 480), (51, -240), (63, 240), (65, -160), (79, 480), (110, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row68 line 214

Source comment

Selected source equation 73 in the original pair table.

def row68 : Integer.Sparse (Fin 271) := [(1, 42), (2, -35), (3, -448), (4, -64), (5, 44), (6, -5), (7, -112), (8, -32), (12, -128), (13, -272), (26, -160), (33, -80), (34, -160), (50, 96), (51, -112), (53, 48), (63, 48), (65, -32)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row69 line 217

Source comment

Selected source equation 77 in the original pair table.

def row69 : Integer.Sparse (Fin 271) := [(0, 5), (1, -73), (2, 44), (3, 160), (4, 64), (5, -15), (7, 20), (8, 40), (10, -36), (12, 56), (13, 32), (23, -120), (24, -336), (27, 123), (29, -192), (54, -192), (77, 36), (78, 72)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row70 line 220

Source comment

Selected source equation 78 in the original pair table.

def row70 : Integer.Sparse (Fin 271) := [(0, 17), (1, -570), (2, 730), (3, 3040), (4, 1040), (5, -620), (6, 15), (7, 1120), (8, 1760), (12, 400), (23, -480), (24, -1440), (26, 480), (27, 600), (29, -960), (34, 160), (50, -3600), (53, -960), (54, -480), (55, -1920), (75, 720), (76, 1440), (143, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row71 line 223

Source comment

Selected source equation 79 in the original pair table.

def row71 : Integer.Sparse (Fin 271) := [(0, -3), (1, 20), (2, 240), (3, 560), (5, -350), (6, 20), (7, 600), (8, 520), (10, -180), (12, 180), (13, 240), (23, -60), (27, 45), (29, -120), (34, 240), (50, -480), (51, 160), (53, -240), (58, -480), (70, 180), (72, 360), (73, 360), (132, -180)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row72 line 226

Source comment

Selected source equation 80 in the original pair table.

def row72 : Integer.Sparse (Fin 271) := [(0, -14), (1, 260), (2, 1255), (3, 3120), (4, 400), (5, -2280), (6, 205), (7, 3040), (8, 2720), (26, 480), (34, 2240), (51, 2320), (79, -960), (82, 720), (83, 1440), (84, 1440), (143, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row73 line 229

Source comment

Selected source equation 81 in the original pair table.

def row73 : Integer.Sparse (Fin 271) := [(0, -17), (1, 80), (2, 990), (3, 2880), (4, 320), (5, -1580), (6, 95), (7, 2800), (8, 2640), (10, -720), (12, 400), (13, 640), (24, -480), (27, 180), (29, -240), (34, 1440), (50, -1920), (51, 640), (55, -960), (58, -1920), (71, 720), (72, 720), (73, 720), (74, 1440), (133, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row74 line 232

Source comment

Selected source equation 82 in the original pair table.

def row74 : Integer.Sparse (Fin 271) := [(0, -17), (1, 280), (2, 1440), (3, 3840), (5, -2160), (6, 185), (7, 2480), (8, 2400), (12, 480), (13, 640), (34, 2400), (51, 3200), (71, 720), (73, 1440), (79, -960), (84, 2880), (133, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row75 line 235

Source comment

Selected source equation 83 in the original pair table.

def row75 : Integer.Sparse (Fin 271) := [(0, -3), (1, 10), (2, 950), (3, 3360), (4, 720), (5, -1240), (6, 95), (7, 1520), (8, 1600), (26, 960), (34, 960), (51, 1280), (79, -1920), (81, 720), (83, 2880), (84, 1440), (143, -1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row76 line 238

Source comment

Selected source equation 84 in the original pair table.

def row76 : Integer.Sparse (Fin 271) := [(0, 13), (1, -580), (2, 285), (3, 4800), (4, 800), (5, -100), (7, 560), (8, 160), (10, -240), (12, 1920), (13, 1520), (23, -1920), (24, -1440), (25, -240), (27, 420), (46, 2880), (47, 1440), (49, 720), (50, -1440), (54, -960), (58, -480), (77, 720), (87, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row77 line 241

Source comment

Selected source equation 85 in the original pair table.

def row77 : Integer.Sparse (Fin 271) := [(0, 8), (1, -124), (2, 37), (3, 800), (4, 352), (5, -12), (6, 1), (7, 64), (12, 592), (13, 80), (23, -96), (25, -384), (26, 128), (32, -96), (34, 64), (42, 576), (49, 144), (51, 32), (54, -96), (96, 288), (103, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row78 line 244

Source comment

Selected source equation 87 in the original pair table.

def row78 : Integer.Sparse (Fin 271) := [(0, 64), (1, -710), (2, 515), (3, 3760), (4, 1760), (5, -260), (6, 5), (7, 480), (8, 800), (12, 240), (23, -240), (24, -480), (26, 880), (27, 60), (30, -1680), (42, 720), (45, 1440), (50, -1440), (51, 80), (55, -960), (75, 720), (79, -480), (98, 1440), (99, 1440), (109, 1440), (143, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row79 line 247

Source comment

Selected source equation 88 in the original pair table.

def row79 : Integer.Sparse (Fin 271) := [(0, 6), (1, -189), (2, 83), (3, 832), (4, 368), (5, -28), (6, 2), (7, 112), (8, 16), (12, 320), (13, 96), (23, -48), (24, -48), (25, -336), (26, 128), (30, -336), (32, -336), (34, 80), (42, 288), (45, 288), (49, 144), (50, -96), (51, 64), (54, -96), (79, -96), (88, 144), (96, 144), (103, 288), (109, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row80 line 250

Source comment

Selected source equation 89 in the original pair table.

def row80 : Integer.Sparse (Fin 271) := [(0, -1), (1, -56), (2, 56), (3, 464), (4, 80), (5, -40), (6, 1), (7, 80), (8, 80), (10, -72), (12, 184), (13, 192), (24, -48), (26, 32), (34, 32), (37, 72), (39, 144), (50, -48), (51, 48), (54, -72), (58, -144), (70, 72), (73, 144), (87, 144), (88, 288), (94, 288), (132, -24)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row81 line 253

Source comment

Selected source equation 90 in the original pair table.

def row81 : Integer.Sparse (Fin 271) := [(0, 31), (1, -362), (2, 90), (3, 768), (4, 704), (5, -20), (6, 1), (7, 32), (8, 32), (12, 144), (24, -96), (25, -240), (26, 160), (30, -768), (34, 32), (42, 288), (43, 576), (51, 32), (54, -96), (88, 288), (103, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row82 line 256

Source comment

Selected source equation 91 in the original pair table.

def row82 : Integer.Sparse (Fin 271) := [(0, 68), (1, -1405), (2, 540), (3, 5040), (4, 2240), (5, -180), (6, 5), (7, 880), (8, 160), (10, -240), (12, 2480), (13, 160), (23, -2160), (24, -1440), (25, -480), (26, 640), (27, 420), (30, -1440), (34, 240), (42, 2880), (51, 160), (54, -1200), (77, 720), (88, 1440), (103, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row83 line 259

Source comment

Selected source equation 92 in the original pair table.

def row83 : Integer.Sparse (Fin 271) := [(0, 54), (1, -935), (2, 310), (3, 3280), (4, 1480), (5, -140), (6, 5), (7, 360), (8, 360), (12, 1080), (23, -480), (24, -120), (26, 720), (27, 30), (30, -240), (34, 80), (42, 720), (44, 1440), (50, -600), (54, -240), (55, -480), (75, 360), (97, 720), (99, 720), (143, -120)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row84 line 262

Source comment

Selected source equation 93 in the original pair table.

def row84 : Integer.Sparse (Fin 271) := [(0, 4), (1, -875), (2, 605), (3, 5680), (4, 640), (5, -420), (6, 20), (7, 880), (8, 640), (10, -720), (12, 3120), (13, 3840), (23, -480), (26, 320), (32, -1920), (34, 800), (35, 720), (37, 1440), (39, 1440), (51, 640), (53, -1200), (54, -720), (58, -960), (70, 720), (73, 1440), (132, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row85 line 265

Source comment

Selected source equation 94 in the original pair table.

def row85 : Integer.Sparse (Fin 271) := [(0, 8), (1, -1045), (2, 155), (3, 6480), (4, 1920), (10, -720), (12, 3200), (13, 2800), (23, -480), (24, -960), (25, -720), (27, 60), (32, -1920), (49, 1440), (54, -1920), (58, -720), (77, 720), (78, 1440), (87, 720), (93, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row86 line 268

Source comment

Selected source equation 95 in the original pair table.

def row86 : Integer.Sparse (Fin 271) := [(0, -7), (1, -515), (2, 435), (3, 4560), (4, 800), (5, -100), (6, 5), (7, 480), (12, 3200), (13, 3600), (25, -240), (26, 160), (32, -960), (34, 800), (40, 1440), (51, 640), (58, -720), (71, 720), (73, 1440), (87, 720), (93, 1440), (133, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row87 line 271

Source comment

Selected source equation 96 in the original pair table.

def row87 : Integer.Sparse (Fin 271) := [(0, -22), (1, -465), (2, 365), (3, 4880), (4, 320), (5, -180), (7, 720), (8, 320), (10, -240), (12, 2800), (13, 3920), (23, -720), (25, -240), (27, 180), (32, -960), (34, 320), (37, 1440), (50, -1920), (53, -1920), (54, -480), (58, -1680), (70, 720), (72, 1440), (87, 720), (93, 1440), (132, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row88 line 274

Source comment

Selected source equation 97 in the original pair table.

def row88 : Integer.Sparse (Fin 271) := [(0, 6), (1, -140), (2, 225), (3, 2560), (4, 800), (5, -260), (6, 15), (7, 1360), (8, 160), (12, 1600), (13, 1040), (23, -480), (25, -960), (26, 720), (34, 1200), (37, 1440), (40, 720), (42, 1440), (51, 560), (53, -720), (82, 720), (89, 1440), (90, 1440), (143, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row89 line 277

Source comment

Selected source equation 98 in the original pair table.

def row89 : Integer.Sparse (Fin 271) := [(0, 39), (1, -385), (2, 615), (3, 3600), (4, 960), (5, -740), (6, 65), (7, 720), (8, 1120), (12, 560), (13, 240), (23, -240), (26, 640), (30, -720), (32, -480), (34, 560), (43, 1440), (50, -1440), (51, 880), (53, -960), (79, -480), (88, 720), (91, 1440), (92, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row90 line 280

Source comment

Selected source equation 99 in the original pair table.

def row90 : Integer.Sparse (Fin 271) := [(0, 24), (1, -795), (2, 495), (3, 4320), (4, 2000), (5, -220), (6, 10), (7, 800), (8, 160), (12, 1120), (13, 960), (25, -960), (26, 1280), (30, -1200), (32, -960), (34, 720), (37, 720), (38, 1440), (40, 1440), (45, 1440), (50, -480), (51, 640), (53, -720), (79, -480), (82, 720), (83, 1440), (88, 720), (95, 1440), (143, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row91 line 283

Source comment

Selected source equation 100 in the original pair table.

def row91 : Integer.Sparse (Fin 271) := [(0, 44), (1, -690), (2, 385), (3, 4960), (4, 2480), (5, -260), (6, 15), (7, 640), (8, 480), (12, 240), (13, 160), (24, -480), (26, 2160), (30, -480), (34, 320), (36, 2160), (39, 1440), (51, 160), (55, -1200), (79, -960), (81, 720), (83, 1440), (91, 1440), (99, 1440), (143, -960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row92 line 286

Source comment

Selected source equation 101 in the original pair table.

def row92 : Integer.Sparse (Fin 271) := [(0, -1), (1, -390), (2, 480), (3, 3520), (4, 1120), (5, -420), (6, 35), (7, 1200), (8, 240), (12, 880), (13, 720), (23, -240), (24, -240), (25, -480), (26, 880), (30, -720), (32, -1440), (34, 1200), (40, 720), (42, 1440), (50, -720), (51, 1120), (53, -480), (58, -480), (71, 720), (79, -480), (87, 1440), (88, 720), (95, 1440), (96, 1440), (133, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row93 line 289

Source comment

Selected source equation 102 in the original pair table.

def row93 : Integer.Sparse (Fin 271) := [(0, 23), (1, -385), (2, 310), (3, 1720), (4, 760), (5, -210), (6, 10), (7, 280), (8, 360), (12, 160), (13, 80), (24, -240), (25, -240), (26, 400), (30, -720), (32, -600), (34, 120), (38, 720), (41, 720), (43, 360), (51, 200), (53, -240), (55, -120), (79, -240), (83, 360), (84, 360), (89, 360), (91, 720), (92, 360), (143, -120)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row94 line 292

Source comment

Selected source equation 103 in the original pair table.

def row94 : Integer.Sparse (Fin 271) := [(0, 21), (1, -255), (2, 170), (3, 880), (4, 432), (5, -88), (6, 4), (7, 80), (8, 192), (26, 288), (29, -96), (30, -96), (34, 32), (39, 288), (51, 80), (55, -96), (56, 288), (79, -96), (83, 144), (84, 144), (99, 288), (143, -48), (149, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row95 line 295

Source comment

Selected source equation 104 in the original pair table.

def row95 : Integer.Sparse (Fin 271) := [(0, 3), (1, -113), (2, 53), (3, 640), (4, 240), (5, -26), (6, 1), (7, 72), (8, 32), (12, 200), (13, 144), (25, -72), (26, 176), (32, -120), (34, 80), (36, 144), (37, 144), (38, 288), (39, 288), (50, -48), (51, 64), (53, -48), (54, -240), (79, -48), (82, 72), (83, 144), (86, 144), (96, 72), (143, -72)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row96 line 298

Source comment

Selected source equation 105 in the original pair table.

def row96 : Integer.Sparse (Fin 271) := [(0, 7), (1, -235), (2, 111), (3, 1424), (4, 464), (5, -60), (6, 3), (7, 160), (8, 96), (12, 352), (13, 144), (23, -96), (25, -144), (26, 416), (30, -96), (32, -480), (34, 80), (35, 288), (36, 288), (38, 576), (39, 576), (51, 32), (53, -144), (54, -480), (79, -192), (81, 144), (83, 288), (85, 288), (92, 288), (143, -192)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row97 line 301

Source comment

Selected source equation 106 in the original pair table.

def row97 : Integer.Sparse (Fin 271) := [(0, 11), (1, -185), (2, 160), (3, 1680), (4, 360), (5, -90), (7, 480), (8, 120), (12, 880), (13, 80), (23, -360), (24, -600), (25, -360), (27, 180), (30, -240), (32, -240), (34, 80), (47, 360), (50, -600), (53, -240), (92, 720), (97, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row98 line 304

Source comment

Selected source equation 107 in the original pair table.

def row98 : Integer.Sparse (Fin 271) := [(0, 21), (1, -333), (2, 124), (3, 1072), (4, 672), (5, -36), (7, 192), (8, 48), (12, 192), (23, -144), (24, -240), (25, -288), (26, 128), (27, 72), (30, -672), (34, 32), (45, 576), (46, 144), (50, -240), (53, -96), (89, 288), (98, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row99 line 307

Source comment

Selected source equation 108 in the original pair table.

def row99 : Integer.Sparse (Fin 271) := [(0, -18), (1, -560), (2, 555), (3, 5200), (4, 720), (5, -440), (6, 25), (7, 1200), (8, 560), (10, -720), (12, 2240), (13, 3200), (26, 640), (32, -960), (34, 1040), (36, 720), (38, 720), (39, 720), (40, 1440), (50, -960), (51, 800), (53, -480), (54, -720), (58, -960), (71, 720), (72, 720), (73, 720), (88, 1440), (94, 720), (95, 720), (133, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row100 line 310

Source comment

Selected source equation 128 in the original pair table.

def row100 : Integer.Sparse (Fin 271) := [(0, 4), (1, -44), (2, 7), (5, -12), (6, 3), (23, -144), (25, -144), (27, 84), (29, -144), (30, -288), (62, -96), (66, 24), (97, 432), (111, -144), (130, -48), (146, -288), (147, -144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row101 line 313

Source comment

Selected source equation 129 in the original pair table.

def row101 : Integer.Sparse (Fin 271) := [(0, 6), (1, -53), (2, 119), (3, 240), (5, -112), (6, 6), (7, 144), (8, 288), (12, 96), (13, 32), (23, -144), (27, 108), (29, -288), (34, 32), (50, -288), (53, -144), (66, 24), (111, -144), (130, -48), (146, -288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row102 line 316

Source comment

Selected source equation 130 in the original pair table.

def row102 : Integer.Sparse (Fin 271) := [(0, 37), (1, -930), (2, 975), (3, 4880), (4, 1360), (5, -840), (6, 40), (7, 1760), (8, 1920), (12, 960), (13, 480), (23, -480), (24, -1440), (26, 640), (27, 600), (29, -960), (30, -960), (34, 800), (50, -4320), (51, 320), (53, -960), (54, -480), (55, -1200), (88, 1440), (89, 720), (99, 1440), (148, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row103 line 319

Source comment

Selected source equation 131 in the original pair table.

def row103 : Integer.Sparse (Fin 271) := [(0, -1), (1, 110), (2, 5), (14, 2160), (23, -2400), (25, -1440), (62, -1440), (66, 60), (111, -960), (116, 1440), (130, -480), (144, 2160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row104 line 322

Source comment

Selected source equation 133 in the original pair table.

def row104 : Integer.Sparse (Fin 271) := [(0, -2), (1, -455), (2, 195), (3, 3040), (4, 720), (5, -80), (7, 480), (12, 1840), (13, 480), (15, 2160), (23, -2160), (24, -720), (25, -1440), (27, 420), (32, -1440), (34, 160), (50, -1440), (53, -1440), (62, -480), (66, 60), (111, -720), (113, -240), (124, 1440), (130, -480), (136, 2160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row105 line 325

Source comment

Selected source equation 134 in the original pair table.

def row105 : Integer.Sparse (Fin 271) := [(0, 8), (1, -30), (2, 25), (5, -12), (6, 3), (17, 432), (23, -288), (25, -624), (27, 48), (29, -144), (30, -576), (62, -96), (66, 12), (85, 432), (100, 432), (110, -432), (111, -144), (130, -96), (134, 432), (140, 288), (142, -144), (146, -48), (147, -144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row106 line 328

Source comment

Selected source equation 135 in the original pair table.

def row106 : Integer.Sparse (Fin 271) := [(0, 52), (1, -425), (2, 55), (17, 2160), (23, -1440), (25, -3600), (27, 480), (29, -960), (30, -4080), (62, -960), (97, 2160), (100, 2160), (110, -720), (145, 1440), (147, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row107 line 331

Source comment

Selected source equation 138 in the original pair table.

def row107 : Integer.Sparse (Fin 271) := [(0, -9), (1, -845), (2, 530), (3, 6960), (5, -160), (7, 960), (12, 3440), (13, 4560), (16, 2160), (23, -2880), (27, 540), (34, 320), (37, 4320), (50, -2880), (53, -2880), (54, -1440), (66, 60), (111, -720), (112, -240), (120, 2160), (121, 1440), (130, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row108 line 334

Source comment

Selected source equation 139 in the original pair table.

def row108 : Integer.Sparse (Fin 271) := [(0, 101), (1, -2045), (2, 420), (3, 8560), (4, 3280), (5, -20), (7, 240), (12, 2640), (13, 480), (18, 2160), (23, -1440), (24, -1440), (25, -1440), (26, 1760), (27, 240), (30, -1440), (32, -1440), (34, 160), (42, 4320), (46, 2160), (50, -240), (54, -1440), (62, -480), (123, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row109 line 337

Source comment

Selected source equation 140 in the original pair table.

def row109 : Integer.Sparse (Fin 271) := [(0, 149), (1, -2280), (2, 265), (3, 6960), (4, 5280), (5, -40), (7, 480), (12, 1200), (13, 320), (23, -1440), (24, -1440), (25, -3600), (26, 2400), (27, 240), (30, -3600), (34, 560), (43, 4320), (54, -2160), (62, -480), (100, 2160), (110, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row110 line 340

Source comment

Selected source equation 144 in the original pair table.

def row110 : Integer.Sparse (Fin 271) := [(0, 32), (1, -25), (2, 95), (5, -60), (14, 1080), (17, 2160), (23, -1920), (25, -2880), (27, 480), (29, -720), (30, -2160), (62, -240), (100, 2160), (110, -720), (111, -480), (116, 720), (134, 4320), (144, 2160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row111 line 343

Source comment

Selected source equation 145 in the original pair table.

def row111 : Integer.Sparse (Fin 271) := [(0, 31), (1, -354), (2, 141), (3, 704), (4, 384), (5, -24), (12, 320), (13, 64), (15, 432), (20, 864), (23, -144), (24, -432), (27, 180), (29, -288), (50, -288), (51, 96), (113, -192), (124, 288), (136, 864), (138, 1728)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row112 line 346

Source comment

Selected source equation 146 in the original pair table.

def row112 : Integer.Sparse (Fin 271) := [(0, 23), (1, -885), (2, 210), (3, 3840), (4, 1200), (12, 1840), (13, 960), (16, 1080), (17, 2160), (23, -1080), (26, 480), (34, 240), (37, 1080), (39, 2160), (50, -720), (51, 240), (54, -1800), (112, -480), (120, 2160), (121, 720), (126, 4320)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row113 line 349

Source comment

Selected source equation 147 in the original pair table.

def row113 : Integer.Sparse (Fin 271) := [(0, -1), (1, -11), (2, 21), (5, -24), (6, 3), (17, 216), (23, -72), (25, -96), (27, 90), (28, 432), (29, -360), (30, -144), (134, 432), (140, 144), (146, -96), (150, 864)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row114 line 352

Source comment

Selected source equation 150 in the original pair table.

def row114 : Integer.Sparse (Fin 271) := [(0, 3), (1, -290), (2, 165), (3, 2080), (4, 640), (5, -60), (7, 320), (12, 1120), (15, 1440), (23, -1680), (24, -1440), (25, -1200), (27, 360), (32, -480), (47, 1440), (50, -480), (54, -960), (66, 60), (111, -480), (113, -480), (117, 1440), (131, -480), (136, 1440), (144, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row115 line 355

Source comment

Selected source equation 151 in the original pair table.

def row115 : Integer.Sparse (Fin 271) := [(0, 17), (1, -725), (2, 260), (3, 4720), (4, 1120), (5, -120), (7, 640), (12, 2000), (13, 560), (16, 720), (23, -2880), (24, -1920), (27, 540), (46, 2880), (50, -960), (54, -1920), (66, 60), (111, -240), (112, -720), (113, -480), (120, 2160), (136, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row116 line 358

Source comment

Selected source equation 152 in the original pair table.

def row116 : Integer.Sparse (Fin 271) := [(0, 9), (1, -160), (2, 40), (3, 1160), (4, 440), (5, -5), (7, 60), (12, 780), (13, 80), (23, -120), (25, -660), (26, 200), (32, -360), (37, 180), (42, 720), (49, 180), (53, -60), (63, -120), (101, 360)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row117 line 361

Source comment

Selected source equation 153 in the original pair table.

def row117 : Integer.Sparse (Fin 271) := [(0, 47), (1, -1150), (2, 350), (3, 4640), (4, 2480), (5, -120), (6, 5), (7, 240), (8, 160), (12, 1120), (21, 1440), (23, -480), (24, -960), (25, -240), (26, 720), (27, 360), (30, -1680), (32, -480), (34, 160), (42, 720), (46, 1440), (47, 720), (50, -2880), (51, 240), (53, -480), (55, -1200), (89, 720), (129, 1440), (139, 1440), (148, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row118 line 364

Source comment

Selected source equation 156 in the original pair table.

def row118 : Integer.Sparse (Fin 271) := [(0, 9), (1, -206), (2, 31), (3, 1088), (4, 432), (5, -4), (7, 48), (12, 464), (13, 144), (18, 288), (23, -240), (24, -288), (25, -144), (26, 32), (27, 36), (32, -96), (34, 32), (46, 288), (47, 144), (49, 432), (50, -48), (54, -384), (103, 144), (127, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row119 line 367

Source comment

Selected source equation 157 in the original pair table.

def row119 : Integer.Sparse (Fin 271) := [(0, 32), (1, -825), (2, 235), (3, 4960), (4, 1760), (12, 3520), (13, 1440), (25, -1920), (26, 400), (32, -1440), (33, 160), (40, 720), (42, 2880), (49, 1440), (104, 720), (106, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row120 line 370

Source comment

Selected source equation 158 in the original pair table.

def row120 : Integer.Sparse (Fin 271) := [(0, 29), (1, -340), (2, 105), (3, 1560), (4, 760), (12, 440), (13, 440), (26, 320), (30, -540), (32, -360), (33, 160), (41, 360), (43, 360), (44, 360), (105, 180), (107, 360), (108, 360)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row121 line 373

Source comment

Selected source equation 161 in the original pair table.

def row121 : Integer.Sparse (Fin 271) := [(0, 116), (1, -1215), (2, 325), (3, 3200), (4, 2000), (5, -60), (7, 240), (8, 160), (12, 800), (13, 160), (22, 1440), (26, 480), (30, -2880), (34, 160), (42, 1440), (45, 1440), (46, 720), (48, 1440), (50, -1680), (55, -240), (89, 720), (99, 1440), (135, 1440), (148, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row122 line 376

Source comment

Selected source equation 162 in the original pair table.

def row122 : Integer.Sparse (Fin 271) := [(0, 29), (1, -1090), (2, 335), (3, 4880), (4, 2000), (12, 2080), (13, 1200), (25, -2880), (26, 800), (30, -2160), (32, -2400), (33, 320), (37, 720), (38, 1440), (42, 1440), (45, 1440), (49, 1440), (53, -720), (63, -720), (101, 720), (102, 1440), (105, 720), (106, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row123 line 379

Source comment

Selected source equation 165 in the original pair table.

def row123 : Integer.Sparse (Fin 271) := [(0, 21), (1, -1115), (2, 610), (3, 5520), (4, 2560), (5, -220), (7, 320), (8, 640), (12, 2160), (13, 1360), (15, 1440), (23, -720), (24, -1440), (25, -960), (27, 360), (30, -1920), (32, -2400), (38, 2880), (41, 2880), (50, -2880), (54, -960), (55, -2400), (63, -480), (66, 60), (89, 1440), (101, 1440), (111, -240), (112, -240), (113, -480), (120, 720), (124, 1440), (125, 1440), (131, -480), (148, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row124 line 382

Source comment

Selected source equation 166 in the original pair table.

def row124 : Integer.Sparse (Fin 271) := [(0, 37), (1, -406), (2, 139), (3, 1216), (4, 704), (12, 384), (13, 16), (25, -144), (26, 224), (30, -576), (32, -96), (33, 32), (42, 288), (44, 576), (45, 576), (49, 144), (105, 288), (106, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row125 line 385

Source comment

Selected source equation 167 in the original pair table.

def row125 : Integer.Sparse (Fin 271) := [(0, 126), (1, -2265), (2, 305), (3, 7920), (4, 5120), (5, -20), (7, 240), (12, 2320), (21, 1440), (23, -1200), (24, -1440), (25, -2640), (26, 2000), (27, 180), (30, -1680), (32, -480), (34, 160), (42, 2160), (43, 4320), (46, 720), (47, 1440), (50, -240), (54, -1920), (103, 720), (104, 1440), (129, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row126 line 388

Source comment

Selected source equation 168 in the original pair table.

def row126 : Integer.Sparse (Fin 271) := [(0, 39), (1, -1590), (2, 670), (3, 8160), (4, 2720), (5, -100), (6, 5), (7, 160), (8, 160), (12, 3200), (13, 3440), (18, 1440), (23, -240), (24, -480), (25, -1200), (26, 320), (27, 180), (30, -1920), (32, -2400), (34, 240), (37, 720), (38, 1440), (41, 4320), (46, 720), (50, -2400), (51, 240), (53, -720), (54, -720), (55, -1200), (63, -480), (89, 720), (101, 1440), (122, 1440), (123, 1440), (148, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row127 line 391

Source comment

Selected source equation 169 in the original pair table.

def row127 : Integer.Sparse (Fin 271) := [(0, 102), (1, -1245), (2, 365), (3, 3440), (4, 2120), (12, 1280), (13, 240), (25, -480), (26, 320), (30, -1440), (32, -720), (33, 80), (43, 720), (44, 2160), (45, 720), (104, 360), (105, 720), (108, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row128 line 394

Source comment

Selected source equation 171 in the original pair table.

def row128 : Integer.Sparse (Fin 271) := [(0, 9), (1, -341), (2, 78), (3, 1568), (4, 592), (5, -28), (6, 2), (7, 48), (8, 32), (12, 608), (13, 608), (22, 288), (23, -48), (24, -96), (25, -192), (26, 224), (27, 36), (30, -288), (32, -384), (34, 160), (35, 144), (38, 576), (41, 576), (50, -384), (51, 64), (53, -432), (54, -144), (55, -336), (89, 144), (135, 288), (141, 288), (148, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row129 line 397

Source comment

Selected source equation 173 in the original pair table.

def row129 : Integer.Sparse (Fin 271) := [(0, 9), (1, -307), (2, 90), (3, 1280), (4, 528), (5, -44), (6, 4), (7, 64), (8, 64), (12, 400), (13, 288), (17, 288), (22, 288), (23, -48), (24, -288), (25, -144), (26, 224), (27, 48), (30, -288), (32, -240), (34, 96), (38, 576), (41, 576), (50, -288), (51, 64), (53, -96), (54, -192), (55, -240), (66, 12), (89, 144), (91, 288), (110, -96), (111, -48), (113, -96), (117, 144), (126, 288), (131, -144), (135, 288), (140, 288), (141, 288), (147, -96), (148, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row130 line 400

Source comment

Selected source equation 175 in the original pair table.

def row130 : Integer.Sparse (Fin 271) := [(0, 53), (1, -1175), (2, 470), (3, 4400), (4, 2400), (5, -160), (7, 480), (8, 320), (12, 1520), (15, 720), (23, -1680), (24, -1680), (25, -3360), (26, 320), (27, 420), (30, -2880), (32, -1200), (43, 1440), (47, 2880), (50, -1920), (53, -960), (54, -960), (63, -480), (66, 60), (92, 1440), (112, -720), (113, -720), (117, 1440), (125, 720), (137, 1440), (148, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row131 line 403

Source comment

Selected source equation 176 in the original pair table.

def row131 : Integer.Sparse (Fin 271) := [(0, 54), (1, -1555), (2, 420), (3, 6320), (4, 3040), (5, -100), (6, 5), (7, 320), (8, 80), (12, 2400), (13, 560), (18, 720), (23, -960), (24, -480), (25, -3360), (26, 720), (27, 240), (30, -2640), (32, -1200), (34, 240), (42, 720), (43, 720), (46, 720), (47, 1440), (49, 1440), (50, -2160), (51, 240), (53, -960), (54, -480), (55, -480), (63, -480), (92, 720), (96, 720), (122, 720), (127, 1440), (139, 720), (148, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row132 line 406

Source comment

Selected source equation 183 in the original pair table.

def row132 : Integer.Sparse (Fin 271) := [(0, 2), (1, -173), (2, 136), (3, 1264), (4, 480), (5, -72), (6, 3), (7, 240), (8, 112), (12, 128), (13, 128), (15, 144), (23, -48), (24, -192), (25, -96), (26, 528), (27, 36), (30, -192), (32, -384), (33, 112), (34, 80), (36, 288), (50, -288), (51, 32), (54, -144), (63, -96), (66, 12), (99, 288), (102, 288), (112, -48), (113, -144), (117, 288), (118, 144), (125, 144), (126, 144), (131, -48), (146, -48), (148, -96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row133 line 409

Source comment

Selected source equation 184 in the original pair table.

def row133 : Integer.Sparse (Fin 271) := [(0, 103), (1, -1580), (2, 560), (3, 7920), (4, 3840), (5, -40), (6, 5), (12, 720), (13, 480), (18, 720), (26, 3920), (30, -480), (32, -960), (33, 720), (34, 160), (51, 160), (52, 1440), (54, -480), (56, 1440), (107, 1440), (119, 720), (127, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row134 line 412

Source comment

Selected source equation 187 in the original pair table.

def row134 : Integer.Sparse (Fin 271) := [(0, 71), (1, -1455), (2, 410), (3, 8000), (4, 3920), (5, -80), (6, 10), (7, 160), (8, 80), (12, 560), (13, 560), (21, 720), (26, 4080), (30, -960), (32, -1440), (33, 720), (34, 320), (36, 1440), (39, 720), (50, -240), (51, 80), (52, 1440), (54, -720), (55, -480), (56, 720), (107, 1440), (128, 720), (135, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row135 line 415

Source comment

Selected source equation 240 in the original pair table.

def row135 : Integer.Sparse (Fin 271) := [(0, 1), (1, -49), (2, -91), (3, -48), (5, 276), (6, -54), (7, -48), (8, -96), (9, 284), (34, -96), (51, -192), (57, -11), (67, -96), (68, -32), (69, -192), (164, -48), (183, -144), (222, -192), (247, 144), (268, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row136 line 418

Source comment

Selected source equation 241 in the original pair table.

def row136 : Integer.Sparse (Fin 271) := [(0, 9), (1, -255), (2, -530), (3, -480), (5, 1520), (6, -180), (7, -1920), (8, -1920), (9, 740), (34, -640), (57, -20), (67, -2400), (68, -1280), (69, -3840), (163, 720), (164, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row137 line 421

Source comment

Selected source equation 242 in the original pair table.

def row137 : Integer.Sparse (Fin 271) := [(1, 3), (2, -28), (3, -192), (4, -48), (5, 76), (6, -12), (7, -144), (9, 28), (11, -48), (26, -96), (34, -224), (51, -144), (57, -1), (67, -96), (68, -64), (143, 144), (164, -48), (183, -48), (222, -96), (247, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row138 line 424

Source comment

Selected source equation 243 in the original pair table.

def row138 : Integer.Sparse (Fin 271) := [(0, -1), (1, 70), (2, -25), (3, -1440), (4, -480), (5, 420), (6, -75), (9, 100), (11, -480), (26, -960), (34, -1440), (51, -1280), (54, 720), (57, -5), (143, 1440), (164, -80), (248, 720), (249, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row139 line 427

Source comment

Selected source equation 244 in the original pair table.

def row139 : Integer.Sparse (Fin 271) := [(0, 6), (1, -105), (2, -260), (3, -1440), (5, 480), (6, -90), (7, -480), (9, 120), (12, -480), (13, -2160), (34, -1680), (51, -1440), (53, 720), (57, -5), (67, -240), (68, -160), (80, -1280), (115, -1200), (132, 1440), (133, 1440), (164, -320), (183, -240), (219, 720), (222, -480), (246, 480), (247, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row140 line 430

Source comment

Selected source equation 245 in the original pair table.

def row140 : Integer.Sparse (Fin 271) := [(0, 1), (1, -80), (2, -270), (3, -480), (4, -80), (5, 560), (6, -60), (7, -720), (8, -800), (9, 180), (34, -160), (50, 720), (51, -240), (57, -5), (67, -480), (68, -160), (69, -960), (181, 720), (182, 480), (183, -80)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row141 line 433

Source comment

Selected source equation 246 in the original pair table.

def row141 : Integer.Sparse (Fin 271) := [(0, 6), (1, -185), (2, -235), (3, -400), (4, -80), (5, 440), (6, -90), (8, -320), (9, 300), (11, -80), (13, -320), (26, -160), (34, -480), (51, -880), (55, 480), (57, -10), (67, -80), (69, -320), (80, -320), (115, -400), (133, 960), (143, 240), (164, -80), (183, -160), (219, 240), (222, -160), (263, 960), (268, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row142 line 436

Source comment

Selected source equation 247 in the original pair table.

def row142 : Integer.Sparse (Fin 271) := [(0, -1), (1, -15), (2, -190), (3, -640), (4, -160), (5, 320), (6, -35), (7, -480), (8, -320), (9, 100), (26, -160), (27, -60), (34, -320), (50, 480), (51, -480), (57, -5), (66, -60), (67, -320), (69, -160), (111, 240), (113, 480), (181, 480), (183, -160), (220, 480), (222, -160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row143 line 439

Source comment

Selected source equation 248 in the original pair table.

def row143 : Integer.Sparse (Fin 271) := [(0, 1), (1, 60), (2, -15), (3, -1120), (4, -320), (5, 420), (6, -25), (9, 60), (11, -320), (26, -800), (27, -120), (34, -1120), (51, -320), (54, 240), (57, -5), (66, -120), (148, 960), (164, -80), (220, 480), (222, -160), (248, 240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row144 line 442

Source comment

Selected source equation 249 in the original pair table.

def row144 : Integer.Sparse (Fin 271) := [(0, 7), (1, -55), (2, -175), (3, -1040), (5, 460), (6, -60), (7, -400), (8, -160), (9, 80), (12, -320), (13, -1360), (34, -720), (50, 480), (51, -960), (53, 240), (57, -5), (66, -60), (67, -160), (68, -160), (69, -80), (80, -320), (112, 480), (113, 240), (115, -400), (164, -80), (182, 480), (183, -160), (219, 240), (221, 480), (222, -160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row145 line 445

Source comment

Selected source equation 250 in the original pair table.

def row145 : Integer.Sparse (Fin 271) := [(0, 1), (1, 64), (2, -38), (3, -640), (4, -192), (5, 24), (6, -3), (12, -192), (13, -256), (26, -192), (27, -36), (34, -192), (50, 576), (51, -192), (54, 576), (114, 144), (115, -48), (220, 576), (221, 384), (222, -64)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row146 line 448

Source comment

Selected source equation 251 in the original pair table.

def row146 : Integer.Sparse (Fin 271) := [(0, 3), (1, -45), (2, -200), (3, -400), (5, 700), (6, -60), (7, -80), (8, -480), (9, 160), (27, -180), (51, -480), (57, -10), (66, -180), (67, -80), (69, -400), (113, 240), (146, 480), (147, 480), (181, 240), (183, -80)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row147 line 451

Source comment

Selected source equation 252 in the original pair table.

def row147 : Integer.Sparse (Fin 271) := [(0, 8), (1, -40), (2, -40), (3, -560), (5, 420), (6, -25), (9, 60), (11, -160), (12, -80), (13, -720), (26, -320), (34, -880), (51, -560), (54, 240), (57, -5), (66, -120), (80, -160), (115, -160), (147, 480), (164, -80), (221, 480), (222, -160), (249, 240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row148 line 454

Source comment

Selected source equation 253 in the original pair table.

def row148 : Integer.Sparse (Fin 271) := [(0, 6), (1, -5), (2, -15), (3, -480), (4, -80), (5, 480), (6, -30), (7, -160), (8, -160), (9, 140), (11, -160), (13, -320), (26, -480), (34, -960), (51, -160), (55, 240), (57, -10), (66, -180), (68, -160), (69, -240), (80, -160), (131, 480), (146, 240), (148, 240), (164, -80), (182, 240), (183, -80), (263, 240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row149 line 457

Source comment

Selected source equation 261 in the original pair table.

def row149 : Integer.Sparse (Fin 271) := [(0, 1), (1, -33), (2, -51), (3, -48), (5, 148), (6, -15), (7, -144), (8, -192), (9, 36), (34, -80), (51, -96), (67, -288), (68, -112), (69, -432), (151, 144), (152, -32), (222, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row150 line 460

Source comment

Selected source equation 262 in the original pair table.

def row150 : Integer.Sparse (Fin 271) := [(0, 2), (1, -15), (2, -10), (3, -280), (5, 170), (6, -25), (7, -360), (9, 50), (13, -120), (26, -120), (34, -560), (51, -240), (53, 360), (59, -80), (67, -360), (68, -320), (69, -240), (152, -80), (153, 360), (154, 240), (222, -40)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row151 line 463

Source comment

Selected source equation 263 in the original pair table.

def row151 : Integer.Sparse (Fin 271) := [(0, 9), (1, -225), (2, -300), (3, -480), (4, -80), (5, 840), (6, -100), (7, -320), (8, -960), (9, 80), (13, -320), (26, -80), (34, -400), (50, 240), (51, -880), (55, 480), (58, 480), (67, -560), (68, -80), (69, -1200), (115, -160), (151, 240), (153, 240), (155, 960), (222, -160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row152 line 466

Source comment

Selected source equation 264 in the original pair table.

def row152 : Integer.Sparse (Fin 271) := [(0, 3), (1, -30), (2, -80), (3, -560), (4, -80), (5, 260), (6, -25), (7, -640), (8, -320), (9, 40), (26, -240), (34, -720), (51, -240), (65, -160), (67, -400), (68, -240), (69, -320), (79, 240), (151, 240), (152, -80), (222, -80)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row153 line 469

Source comment

Selected source equation 266 in the original pair table.

def row153 : Integer.Sparse (Fin 271) := [(0, 7), (1, 60), (2, 40), (3, -1280), (5, 140), (6, -35), (7, -480), (9, 20), (12, -240), (13, -640), (26, -800), (33, -480), (34, -1360), (54, 720), (59, -160), (65, -480), (68, -240), (69, -80), (131, 720), (152, -160), (158, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row154 line 472

Source comment

Selected source equation 267 in the original pair table.

def row154 : Integer.Sparse (Fin 271) := [(0, -2), (1, 315), (2, -60), (3, -4080), (4, -960), (5, 220), (6, -45), (7, -960), (9, 20), (13, -1200), (26, -2880), (33, -1280), (34, -2000), (51, -480), (54, 720), (63, 1440), (65, -960), (67, -80), (68, -240), (112, 720), (152, -160), (156, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row155 line 475

Source comment

Selected source equation 268 in the original pair table.

def row155 : Integer.Sparse (Fin 271) := [(0, 3), (1, 20), (2, 35), (3, -480), (5, 200), (6, -40), (7, -480), (9, 80), (13, -160), (26, -480), (33, -160), (34, -960), (53, 480), (65, -320), (67, -160), (68, -320), (69, -160), (111, 240), (130, 240), (131, 480), (152, -160), (153, 480), (156, 480), (222, -160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row156 line 478

Source comment

Selected source equation 269 in the original pair table.

def row156 : Integer.Sparse (Fin 271) := [(0, 6), (1, -65), (2, -125), (3, -1360), (4, -160), (5, 420), (6, -70), (7, -320), (8, -160), (9, 60), (13, -960), (26, -640), (33, -400), (34, -1200), (51, -1040), (55, 480), (59, -400), (63, 240), (65, -160), (67, -240), (68, -160), (69, -160), (112, 480), (113, 240), (115, -320), (131, 240), (152, -160), (154, 240), (155, 480), (158, 480), (222, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row157 line 481

Source comment

Selected source equation 270 in the original pair table.

def row157 : Integer.Sparse (Fin 271) := [(0, 9), (1, -45), (2, -85), (3, -800), (4, -80), (5, 460), (6, -85), (7, -640), (8, -480), (9, 100), (26, -400), (34, -560), (50, 240), (51, -400), (67, -320), (68, -80), (69, -480), (110, 480), (111, 480), (113, 240), (131, 240), (146, 480), (153, 240), (222, -80)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row158 line 484

Source comment

Selected source equation 275 in the original pair table.

def row158 : Integer.Sparse (Fin 271) := [(0, 8), (1, 35), (2, -340), (3, -3120), (4, -800), (5, 680), (6, -55), (7, -1920), (8, -800), (10, 240), (11, -160), (12, -80), (13, -160), (26, -1760), (32, 480), (33, -320), (34, -2640), (51, -800), (54, 240), (65, -800), (79, 1920), (80, -80), (143, 480), (160, 480), (162, -160), (179, 480), (180, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row159 line 487

Source comment

Selected source equation 276 in the original pair table.

def row159 : Integer.Sparse (Fin 271) := [(0, 1), (1, -12), (2, -27), (3, -224), (4, -16), (5, 52), (6, -8), (7, -16), (8, -16), (11, -16), (12, -88), (13, -304), (26, -32), (32, 96), (33, -32), (34, -144), (51, -176), (53, 48), (58, 240), (59, -64), (80, -32), (115, -96), (132, 24), (133, 48), (143, 48), (159, 48), (162, -16), (218, 96), (245, 96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row160 line 490

Source comment

Selected source equation 277 in the original pair table.

def row160 : Integer.Sparse (Fin 271) := [(0, 6), (1, 65), (2, -180), (3, -2880), (4, -720), (5, 440), (6, -35), (7, -1680), (8, -480), (11, -240), (13, -240), (26, -1920), (33, -480), (34, -2800), (51, -720), (59, -160), (65, -960), (79, 1440), (143, 720), (160, 720), (162, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row161 line 493

Source comment

Selected source equation 278 in the original pair table.

def row161 : Integer.Sparse (Fin 271) := [(0, 1), (1, 6), (2, -39), (3, -576), (4, -160), (5, 108), (6, -14), (7, -192), (8, -64), (11, -128), (12, -32), (13, -112), (26, -352), (32, 96), (33, -64), (34, -544), (51, -256), (53, 48), (55, 96), (58, 96), (59, -64), (65, -64), (79, 192), (115, -16), (143, 480), (159, 48), (161, 96), (162, -48), (218, 192), (245, 96)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row162 line 496

Source comment

Selected source equation 285 in the original pair table.

def row162 : Integer.Sparse (Fin 271) := [(0, 7), (1, 105), (2, -120), (3, -1920), (4, -240), (12, -960), (13, -2000), (26, -240), (31, -80), (32, 1440), (33, -480), (50, 720), (51, -240), (59, -240), (60, 720), (114, 720), (115, -240), (217, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row163 line 499

Source comment

Selected source equation 286 in the original pair table.

def row163 : Integer.Sparse (Fin 271) := [(0, 14), (1, -65), (2, -80), (3, -1200), (5, 340), (6, -65), (12, -160), (13, -1280), (26, -240), (32, 240), (33, -160), (34, -560), (51, -1120), (59, -160), (80, -80), (110, 480), (115, -320), (147, 480), (179, 240), (217, 480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row164 line 502

Source comment

Selected source equation 287 in the original pair table.

def row164 : Integer.Sparse (Fin 271) := [(0, 7), (1, -10), (2, -25), (3, -480), (5, 200), (6, -30), (11, -40), (12, -40), (13, -480), (26, -200), (32, 120), (34, -440), (51, -440), (54, 120), (62, 240), (80, -40), (110, 240), (115, -40), (147, 240), (179, 120), (245, 120)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row165 line 505

Source comment

Selected source equation 297 in the original pair table.

def row165 : Integer.Sparse (Fin 271) := [(0, -5), (1, 131), (2, 228), (3, 224), (5, -556), (6, 42), (7, 656), (8, 928), (9, -120), (34, 224), (51, 192), (67, 848), (68, 272), (69, 1664), (151, -576), (163, -144), (165, 144), (166, 576), (167, 576), (247, -144), (268, -288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row166 line 508

Source comment

Selected source equation 298 in the original pair table.

def row166 : Integer.Sparse (Fin 271) := [(0, -23), (1, -195), (2, 220), (3, 3200), (5, -420), (6, 30), (7, 1520), (8, 640), (9, -40), (10, -240), (12, 560), (13, 160), (23, -1920), (24, -960), (26, 320), (27, 420), (34, 800), (50, -1440), (53, -1680), (54, -1440), (67, 400), (68, 240), (69, 160), (75, 2880), (77, 720), (143, -960), (163, -240), (174, 1440), (175, 2160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row167 line 511

Source comment

Selected source equation 300 in the original pair table.

def row167 : Integer.Sparse (Fin 271) := [(0, -19), (1, -115), (2, 430), (3, 3200), (5, -740), (6, 20), (7, 2800), (8, 1280), (9, -40), (10, -720), (12, 720), (13, 960), (23, -240), (24, -480), (27, 180), (34, 2240), (50, -1920), (51, 640), (53, -960), (58, -1920), (67, 720), (68, 400), (69, 320), (70, 720), (71, 1440), (72, 1440), (132, -720), (151, -960), (163, -240), (165, 720), (166, 1440), (247, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row168 line 514

Source comment

Selected source equation 301 in the original pair table.

def row168 : Integer.Sparse (Fin 271) := [(0, -3), (1, 41), (2, 126), (3, 176), (4, 48), (5, -208), (6, 16), (7, 304), (8, 352), (9, -32), (10, -96), (12, 32), (13, 16), (24, -96), (26, 32), (27, 24), (29, -48), (34, 80), (50, -144), (51, 48), (53, -48), (54, -48), (55, -192), (58, -96), (67, 144), (68, 16), (69, 480), (72, 288), (73, 144), (76, 288), (133, -96), (143, -96), (151, -96), (163, -48), (166, 144), (168, 144), (172, 288), (173, 288), (247, -48), (268, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row169 line 517

Source comment

Selected source equation 302 in the original pair table.

def row169 : Integer.Sparse (Fin 271) := [(0, -5), (1, 101), (2, 210), (3, 336), (4, 16), (5, -360), (6, 26), (7, 352), (8, 576), (9, -24), (34, 144), (50, -144), (51, 288), (67, 208), (68, 80), (69, 320), (79, -192), (84, 288), (151, -96), (167, 288), (194, 144), (197, 288), (199, 288), (268, -144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row170 line 520

Source comment

Selected source equation 303 in the original pair table.

def row170 : Integer.Sparse (Fin 271) := [(0, -13), (1, -30), (2, 155), (3, 2000), (5, -580), (6, 70), (7, 1840), (8, 960), (9, -160), (10, -480), (12, 160), (13, 80), (23, -720), (24, -240), (26, 160), (27, 120), (34, 1520), (50, -480), (51, 160), (53, -1200), (54, -240), (58, -480), (67, 1600), (68, 960), (69, 640), (70, 1440), (71, 720), (75, 1440), (132, -480), (143, -480), (151, -480), (163, -240), (165, 720), (168, 720), (170, 1440), (171, 1440), (247, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row171 line 523

Source comment

Selected source equation 304 in the original pair table.

def row171 : Integer.Sparse (Fin 271) := [(0, -11), (1, 10), (2, 605), (3, 3120), (4, 400), (5, -900), (6, 70), (7, 2400), (8, 720), (9, -80), (12, 160), (13, 320), (24, -240), (26, 480), (34, 2320), (50, -480), (51, 1920), (67, 640), (68, 320), (69, 640), (71, 1440), (79, -960), (82, 720), (83, 1440), (133, -480), (143, -720), (151, -1440), (163, -720), (165, 720), (166, 1440), (194, 2160), (199, 1440), (247, -240), (268, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row172 line 526

Source comment

Selected source equation 305 in the original pair table.

def row172 : Integer.Sparse (Fin 271) := [(0, -28), (1, 415), (2, 840), (3, 1760), (4, 400), (5, -1660), (6, 105), (7, 1920), (8, 2880), (9, -120), (13, 320), (26, 160), (34, 800), (50, -1680), (51, 640), (55, -1440), (58, -1200), (67, 1040), (68, 400), (69, 1600), (74, 2880), (75, 720), (133, -960), (143, -240), (151, -480), (167, 1440), (170, 1440), (171, 720), (172, 1440), (247, -240), (268, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row173 line 529

Source comment

Selected source equation 306 in the original pair table.

def row173 : Integer.Sparse (Fin 271) := [(0, -27), (1, 555), (2, 1085), (3, 1600), (4, 80), (5, -2280), (6, 225), (7, 2320), (8, 3040), (9, -160), (26, 160), (34, 880), (50, -720), (51, 1280), (67, 720), (68, 80), (69, 2400), (83, 1440), (143, -480), (151, -480), (163, -240), (166, 720), (194, 720), (197, 1440), (199, 1440), (268, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row174 line 532

Source comment

Selected source equation 307 in the original pair table.

def row174 : Integer.Sparse (Fin 271) := [(0, -9), (1, 20), (2, 95), (3, 800), (5, -180), (6, 20), (7, 480), (9, -40), (12, 160), (13, 160), (23, -240), (30, -480), (32, -480), (34, 320), (51, 320), (67, 160), (68, 160), (79, -960), (88, 1440), (111, -240), (130, -240), (151, -480), (194, 1440), (205, 1440), (268, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row175 line 535

Source comment

Selected source equation 308 in the original pair table.

def row175 : Integer.Sparse (Fin 271) := [(0, -4), (1, 15), (2, 20), (3, 2400), (4, 640), (5, -380), (6, 45), (7, 2560), (8, 480), (9, -40), (12, 320), (13, 160), (23, -480), (24, -480), (25, -1200), (26, 1120), (34, 1440), (51, 320), (53, -1200), (67, 240), (68, 80), (69, 160), (89, 2880), (103, 720), (111, -480), (131, -480), (143, -960), (151, -480), (163, -240), (175, 720), (204, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row176 line 538

Source comment

Selected source equation 311 in the original pair table.

def row176 : Integer.Sparse (Fin 271) := [(0, -3), (1, -76), (2, 172), (3, 1232), (4, 224), (5, -136), (6, 11), (7, 352), (8, 224), (9, -8), (12, 256), (13, 160), (23, -144), (24, -96), (26, 256), (32, -768), (34, 208), (51, 224), (53, -240), (54, -48), (67, 48), (68, 16), (69, 32), (79, -576), (92, 576), (96, 288), (112, -96), (113, -96), (143, -192), (151, -96), (163, -48), (175, 144), (205, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row177 line 541

Source comment

Selected source equation 312 in the original pair table.

def row177 : Integer.Sparse (Fin 271) := [(0, -19), (1, -5), (2, 440), (3, 3680), (4, 160), (5, -1260), (6, 220), (7, 1760), (8, 320), (9, -160), (12, 400), (13, 2080), (23, -240), (26, 480), (34, 2720), (50, -480), (51, 3520), (53, -1200), (67, 560), (68, 400), (69, 160), (95, 2880), (112, -960), (113, -480), (143, -960), (151, -480), (163, -240), (175, 720), (194, 1440), (204, 1440), (268, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row178 line 544

Source comment

Selected source equation 313 in the original pair table.

def row178 : Integer.Sparse (Fin 271) := [(0, -33), (1, 100), (2, 985), (3, 5680), (5, -1360), (6, 170), (7, 1680), (8, 960), (9, -120), (12, 1840), (13, 4720), (23, -720), (34, 2800), (50, -480), (51, 3520), (53, -240), (58, -1200), (67, 560), (68, 400), (69, 160), (90, 1440), (94, 2880), (112, -1440), (113, -480), (133, -960), (151, -480), (171, 720), (199, 1440), (203, 1440), (247, -240), (268, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row179 line 547

Source comment

Selected source equation 314 in the original pair table.

def row179 : Integer.Sparse (Fin 271) := [(0, -19), (1, 50), (2, 170), (3, 2400), (5, -360), (6, 35), (7, 1760), (8, 800), (9, -40), (10, -480), (12, 960), (13, 880), (23, -240), (26, 320), (27, 360), (34, 720), (50, -1200), (51, 160), (54, -1200), (58, -480), (67, 240), (69, 240), (97, 1440), (111, -480), (143, -480), (146, -480), (151, -480), (163, -240), (174, 720), (203, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row180 line 550

Source comment

Selected source equation 315 in the original pair table.

def row180 : Integer.Sparse (Fin 271) := [(0, -3), (1, 14), (2, 7), (3, 368), (5, -36), (6, 16), (7, 448), (8, 96), (9, -40), (10, -48), (12, 80), (13, 64), (23, -144), (26, 96), (27, 36), (34, 208), (50, -48), (53, -48), (54, -240), (67, 160), (68, 64), (69, 96), (85, 288), (111, -240), (130, -96), (131, -48), (143, -288), (146, -96), (163, -48), (168, 144), (174, 144), (247, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row181 line 553

Source comment

Selected source equation 332 in the original pair table.

def row181 : Integer.Sparse (Fin 271) := [(0, 1), (1, -320), (2, 200), (3, 2000), (4, 560), (5, -220), (6, 15), (7, 960), (9, -20), (12, 720), (13, 160), (23, -2160), (24, -2400), (25, -720), (27, 600), (34, 320), (47, 2160), (50, -720), (54, -1440), (62, -480), (66, 240), (67, 240), (68, 160), (111, -1440), (113, -1440), (130, -480), (131, -1440), (181, -240), (242, 1440), (256, 2160)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row182 line 556

Source comment

Selected source equation 337 in the original pair table.

def row182 : Integer.Sparse (Fin 271) := [(0, 54), (1, -660), (2, 935), (3, 4320), (4, 2000), (5, -940), (6, 45), (7, 1920), (8, 1920), (12, 240), (13, 160), (26, 1200), (30, -3600), (34, 800), (42, 2160), (50, -3600), (55, -1440), (75, 2160), (89, 4320), (99, 4320), (143, -240), (148, -2400), (252, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row183 line 559

Source comment

Selected source equation 338 in the original pair table.

def row183 : Integer.Sparse (Fin 271) := [(0, -3), (1, -190), (2, 385), (3, 2880), (4, 720), (5, -560), (6, 30), (7, 1440), (8, 960), (10, -1080), (11, 240), (12, 520), (13, 720), (26, 960), (34, 1120), (37, 1080), (39, 2160), (51, 240), (54, -1080), (58, -720), (70, 1080), (73, 2160), (132, -120), (143, -720), (193, 2160), (229, 720), (232, 4320), (248, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row184 line 562

Source comment

Selected source equation 339 in the original pair table.

def row184 : Integer.Sparse (Fin 271) := [(0, 9), (1, -315), (2, 170), (3, 2880), (4, 960), (5, -680), (6, 120), (7, 960), (9, -20), (11, 480), (12, 240), (26, 960), (32, -2880), (34, 2080), (35, 2160), (39, 4320), (51, 1440), (53, -720), (54, -2160), (67, 240), (68, 160), (143, -1440), (179, -2160), (185, 4320), (223, 2160), (245, -1440), (246, -240), (249, -960), (258, 4320), (260, 1440), (262, 8640)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row185 line 565

Source comment

Selected source equation 340 in the original pair table.

def row185 : Integer.Sparse (Fin 271) := [(0, -29), (1, -490), (2, 485), (3, 3920), (5, -340), (7, 1840), (8, 160), (10, -240), (12, 1200), (13, 320), (23, -3360), (24, -2400), (25, -480), (26, 160), (27, 1020), (32, -480), (34, 160), (50, -2880), (53, -1200), (54, -2400), (64, -480), (77, 720), (87, 720), (109, 2880), (114, -240), (177, 1440), (178, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row186 line 568

Source comment

Selected source equation 343 in the original pair table.

def row186 : Integer.Sparse (Fin 271) := [(0, -12), (1, -405), (2, 300), (3, 3440), (4, 640), (5, -260), (6, 5), (7, 1200), (8, 80), (9, -20), (10, -480), (12, 1040), (13, 320), (23, -3600), (24, -3120), (26, 160), (27, 780), (34, 320), (46, 1440), (50, -480), (51, 160), (54, -3360), (66, 180), (67, 240), (68, 160), (77, 1440), (103, 720), (111, -240), (112, -2160), (113, -1440), (131, -480), (175, 720), (181, -240), (234, 1440), (241, 1440), (248, -240), (256, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row187 line 571

Source comment

Selected source equation 345 in the original pair table.

def row187 : Integer.Sparse (Fin 271) := [(0, 29), (1, -515), (2, 480), (3, 1280), (4, 800), (5, -420), (6, 30), (7, 240), (8, 800), (9, -20), (12, 320), (23, -480), (24, -2880), (27, 1140), (29, -1680), (30, -960), (32, -960), (48, 1440), (50, -720), (51, 80), (54, -1920), (66, 180), (67, 80), (69, 320), (97, 720), (98, 1440), (111, -240), (113, -1680), (131, -960), (146, -1440), (147, -720), (174, 720), (177, 1440), (179, -480), (181, -240), (249, -240), (256, 720), (266, 1440), (267, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row188 line 574

Source comment

Selected source equation 346 in the original pair table.

def row188 : Integer.Sparse (Fin 271) := [(0, -1), (1, -80), (2, 555), (3, 2800), (4, 960), (5, -660), (6, 40), (7, 1040), (8, 1440), (9, -20), (26, 640), (30, -960), (34, 480), (45, 1440), (50, -3360), (51, 480), (55, -1680), (67, 240), (68, 160), (69, 320), (75, 1440), (89, 720), (99, 1440), (143, -480), (148, -720), (155, -960), (170, 720), (182, -720), (199, 1440), (250, 1440), (251, 1440), (263, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row189 line 577

Source comment

Selected source equation 347 in the original pair table.

def row189 : Integer.Sparse (Fin 271) := [(0, 9), (1, -110), (2, 515), (3, 1040), (4, 320), (5, -740), (6, 80), (7, 400), (8, 1600), (9, -20), (12, 400), (23, -240), (27, 300), (29, -480), (32, -960), (44, 2880), (50, -2880), (51, 160), (53, -1440), (67, 80), (69, 640), (153, -960), (168, 720), (176, 1440), (181, -720), (197, 1440), (245, -480), (246, -240), (253, 2880), (254, 2880)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row190 line 580

Source comment

Selected source equation 349 in the original pair table.

def row190 : Integer.Sparse (Fin 271) := [(0, -13), (1, -630), (2, 660), (3, 4800), (4, 960), (5, -660), (6, 35), (7, 1840), (8, 720), (9, -20), (12, 1440), (13, 720), (23, -2160), (24, -1200), (25, -2400), (26, 320), (27, 480), (30, -1920), (32, -960), (34, 1040), (47, 1440), (50, -4080), (51, 640), (53, -3120), (54, -960), (55, -1200), (63, -2400), (66, 180), (67, 240), (68, 160), (89, 720), (92, 4320), (96, 1440), (111, -240), (112, -2160), (113, -1440), (131, -480), (148, -1680), (175, 720), (178, 1440), (180, -480), (182, -240), (234, 720), (238, 1440), (242, 1440), (248, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row191 line 583

Source comment

Selected source equation 350 in the original pair table.

def row191 : Integer.Sparse (Fin 271) := [(0, 18), (1, -520), (2, 425), (3, 2760), (4, 720), (5, -510), (6, 35), (7, 1040), (8, 960), (9, -10), (10, -240), (12, 520), (13, 480), (24, -960), (26, 560), (27, 270), (29, -480), (30, -480), (34, 680), (48, 720), (50, -1080), (51, 80), (54, -840), (66, 90), (67, 40), (69, 160), (80, 80), (88, 720), (99, 1440), (111, -120), (113, -840), (131, -480), (146, -720), (148, -480), (174, 360), (182, -120), (234, 360), (249, -120), (265, 720), (266, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row192 line 586

Source comment

Selected source equation 351 in the original pair table.

def row192 : Integer.Sparse (Fin 271) := [(0, -2), (1, -195), (2, 360), (3, 2960), (4, 520), (5, -550), (6, 65), (7, 440), (8, 480), (9, -10), (11, 80), (12, 720), (13, 1680), (26, 480), (34, 1200), (44, 720), (50, -960), (51, 1360), (53, -480), (55, -480), (67, 120), (68, 80), (69, 160), (94, 1440), (95, 720), (143, -240), (155, -480), (170, 360), (182, -360), (199, 720), (254, 720), (263, -120), (270, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row193 line 589

Source comment

Selected source equation 353 in the original pair table.

def row193 : Integer.Sparse (Fin 271) := [(0, -8), (1, -345), (2, 605), (3, 5600), (4, 1280), (5, -1000), (6, 130), (7, 480), (8, 640), (11, 240), (12, 1280), (13, 2880), (26, 1440), (34, 2160), (42, 1440), (44, 1440), (50, -1200), (51, 2480), (53, -960), (54, -240), (55, -960), (75, 720), (94, 2880), (95, 2880), (143, -960), (240, 1440), (252, 1440), (254, 1440), (270, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row194 line 592

Source comment

Selected source equation 354 in the original pair table.

def row194 : Integer.Sparse (Fin 271) := [(0, -29), (1, 370), (2, 835), (3, 4080), (5, -1460), (6, 210), (7, 1200), (8, 640), (9, -20), (10, -720), (12, 1280), (13, 3840), (32, -960), (34, 2560), (37, 1440), (51, 3040), (53, -960), (58, -960), (67, 240), (68, 160), (70, 720), (73, 1440), (80, 800), (115, 800), (132, -720), (133, -1920), (179, -720), (186, 2880), (223, 720), (229, 1440), (236, 1440), (245, -960), (246, -240), (258, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row195 line 595

Source comment

Selected source equation 355 in the original pair table.

def row195 : Integer.Sparse (Fin 271) := [(0, -1), (1, -370), (2, 105), (3, 2400), (4, 720), (5, -40), (7, 480), (12, 1200), (13, 640), (23, -2160), (24, -2160), (25, -1440), (27, 300), (32, -1440), (34, 320), (54, -2880), (62, -960), (66, 60), (111, -720), (113, -720), (130, -480), (131, -1440), (174, 2160), (177, 2160), (179, -720), (249, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row196 line 598

Source comment

Selected source equation 356 in the original pair table.

def row196 : Integer.Sparse (Fin 271) := [(0, -2), (1, -69), (2, 24), (3, 432), (4, 48), (5, -36), (6, 3), (7, 192), (9, -4), (12, 240), (13, 64), (23, -432), (25, -144), (27, 84), (32, -288), (34, 96), (50, -432), (53, -576), (62, -96), (66, 24), (67, 48), (68, 32), (111, -288), (130, -192), (153, -288), (168, 432), (176, 432), (181, -144), (245, -144), (246, -144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row197 line 601

Source comment

Selected source equation 362 in the original pair table.

def row197 : Integer.Sparse (Fin 271) := [(1, -93), (2, 175), (3, 784), (4, 192), (5, -216), (6, 16), (7, 416), (8, 336), (9, -8), (12, 32), (13, 32), (24, -336), (26, 112), (27, 96), (29, -96), (30, -192), (34, 176), (45, 144), (50, -528), (51, 144), (54, -96), (55, -96), (66, 24), (67, 96), (68, 48), (69, 80), (88, 288), (98, 144), (99, 288), (113, -288), (131, -96), (146, -96), (147, -48), (148, -96), (155, -96), (181, -48), (182, -48), (194, 144), (199, 144), (250, 288), (251, 144), (253, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row198 line 604

Source comment

Selected source equation 363 in the original pair table.

def row198 : Integer.Sparse (Fin 271) := [(0, -7), (1, -580), (2, 570), (3, 6160), (4, 1440), (5, -460), (6, 25), (7, 1440), (8, 480), (10, -720), (12, 2000), (13, 2880), (25, -1440), (26, 1440), (30, -720), (32, -1440), (34, 2080), (37, 2160), (38, 4320), (50, -720), (51, 1520), (53, -2160), (54, -720), (58, -1440), (59, 320), (79, -1440), (80, 240), (82, 2160), (83, 4320), (115, 480), (143, -2160), (184, 2160), (193, 4320), (195, 1440), (201, 4320), (202, 4320), (218, -720), (219, -960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row199 line 607

Source comment

Selected source equation 364 in the original pair table.

def row199 : Integer.Sparse (Fin 271) := [(0, 21), (1, -705), (2, 350), (3, 6240), (4, 2720), (5, -580), (6, 30), (7, 1920), (8, 960), (10, -720), (11, 240), (12, 480), (13, 640), (26, 3120), (34, 2000), (36, 2160), (39, 4320), (51, 240), (54, -720), (55, -2160), (79, -1440), (80, 240), (81, 2160), (83, 4320), (143, -3120), (226, 4320), (232, 4320), (261, 1440), (262, 4320), (263, -960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row200 line 610

Source comment

Selected source equation 365 in the original pair table.

def row200 : Integer.Sparse (Fin 271) := [(1, -78), (2, 19), (3, 432), (4, 96), (5, -64), (6, 9), (7, 144), (9, -4), (11, 48), (12, 144), (23, -144), (25, -288), (26, 96), (27, 36), (30, -288), (32, -576), (34, 224), (35, 432), (38, 864), (50, -288), (51, 144), (53, -720), (54, -144), (66, 12), (67, 48), (68, 32), (85, 432), (110, -288), (111, -144), (130, -96), (142, -144), (143, -144), (147, -144), (153, -288), (168, 432), (179, -288), (181, -144), (185, 432), (188, 864), (223, 864), (231, 864), (245, -432), (246, -336), (249, -48), (259, 864), (260, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row201 line 613

Source comment

Selected source equation 368 in the original pair table.

def row201 : Integer.Sparse (Fin 271) := [(0, 1), (1, -98), (2, 113), (3, 1488), (4, 512), (5, -160), (6, 14), (7, 560), (8, 128), (11, 128), (26, 896), (34, 896), (51, 368), (52, 288), (65, 128), (79, -672), (81, 144), (82, 432), (83, 576), (143, -816), (215, 288), (243, 288), (244, 576)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row202 line 616

Source comment

Selected source equation 369 in the original pair table.

def row202 : Integer.Sparse (Fin 271) := [(0, -9), (1, -25), (2, 600), (3, 4480), (4, 1120), (5, -1400), (6, 190), (7, 2400), (8, 480), (9, -40), (11, 640), (24, -480), (26, 1920), (27, 120), (30, -480), (32, -960), (34, 3520), (36, 1440), (50, -480), (51, 2560), (54, -480), (66, 60), (67, 640), (68, 480), (79, -960), (81, 720), (83, 1440), (91, 1440), (110, -480), (111, -240), (113, -480), (131, -480), (143, -3360), (147, -480), (153, -480), (179, -960), (181, -480), (185, 720), (188, 1440), (194, 1440), (233, 2880), (237, 1440), (245, -720), (249, -240), (261, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row203 line 619

Source comment

Selected source equation 372 in the original pair table.

def row203 : Integer.Sparse (Fin 271) := [(0, -2), (1, -63), (2, 107), (3, 1024), (4, 288), (5, -152), (6, 8), (7, 480), (8, 224), (10, -288), (11, 48), (12, 208), (13, 176), (25, -48), (26, 384), (32, -192), (34, 544), (36, 288), (38, 288), (39, 288), (51, 160), (53, -48), (54, -288), (55, -96), (58, -288), (65, 64), (71, 288), (72, 288), (73, 288), (79, -288), (82, 144), (83, 288), (133, -48), (143, -288), (180, -144), (193, 288), (202, 576), (211, 144), (213, 288), (226, 576), (228, 288), (231, 288), (232, 864), (248, -192)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row204 line 622

Source comment

Selected source equation 373 in the original pair table.

def row204 : Integer.Sparse (Fin 271) := [(0, -11), (1, -15), (2, 415), (3, 4080), (4, 880), (5, -980), (6, 145), (7, 640), (8, 480), (11, 320), (12, 880), (13, 2320), (26, 1280), (32, -960), (34, 2320), (36, 1440), (38, 1440), (39, 1440), (51, 2080), (53, -720), (54, -1440), (55, -480), (79, -960), (80, 320), (81, 720), (83, 1440), (115, 320), (132, -240), (133, -480), (143, -1920), (179, -1440), (185, 1440), (201, 2880), (225, 1440), (233, 1440), (237, 2880), (245, -480), (249, -960), (258, 1440), (259, 1440), (261, 1440), (262, 4320)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row205 line 625

Source comment

Selected source equation 374 in the original pair table.

def row205 : Integer.Sparse (Fin 271) := [(0, 7), (1, -142), (2, 152), (3, 544), (4, 256), (5, -128), (6, 7), (7, 192), (8, 224), (9, -4), (12, 48), (23, -336), (24, -960), (26, 32), (27, 324), (29, -384), (30, -288), (34, 48), (46, 144), (50, -144), (51, 64), (54, -528), (66, 48), (67, 32), (68, 16), (69, 32), (98, 576), (112, -192), (113, -480), (131, -96), (146, -192), (147, -192), (181, -48), (234, 288), (241, 144), (267, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row206 line 628

Source comment

Selected source equation 377 in the original pair table.

def row206 : Integer.Sparse (Fin 271) := [(0, -18), (1, 295), (2, 700), (3, 3040), (4, 160), (5, -1260), (6, 135), (7, 2240), (8, 720), (9, -60), (12, 320), (13, 1440), (23, -240), (26, 160), (27, 60), (34, 3200), (37, 720), (51, 2960), (53, -240), (54, -240), (58, -720), (59, 560), (66, 60), (67, 800), (68, 400), (79, -960), (80, 80), (82, 1440), (90, 720), (112, -720), (113, -480), (115, 400), (133, -240), (143, -480), (147, -240), (154, -480), (171, 720), (179, -480), (181, -240), (195, 1440), (207, 720), (219, -240), (224, 1440), (236, 720), (237, 1440), (249, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row207 line 631

Source comment

Selected source equation 378 in the original pair table.

def row207 : Integer.Sparse (Fin 271) := [(0, -24), (1, 360), (2, 715), (3, 4240), (4, 80), (5, -1360), (6, 175), (7, 1760), (8, 800), (10, -720), (11, 80), (12, 1280), (13, 4400), (26, 160), (32, -480), (34, 3920), (40, 720), (51, 3440), (53, -720), (58, -1920), (59, 640), (71, 720), (72, 720), (73, 720), (79, -480), (80, 960), (82, 720), (115, 1360), (132, -960), (133, -1680), (143, -480), (179, -720), (186, 1440), (196, 1440), (207, 720), (209, 720), (225, 720), (227, 1440), (233, 720), (239, 720), (245, -480), (258, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row208 line 634

Source comment

Selected source equation 379 in the original pair table.

def row208 : Integer.Sparse (Fin 271) := [(0, -31), (1, -330), (2, 410), (3, 6720), (4, 160), (5, -400), (6, 15), (7, 2320), (8, 320), (10, -2640), (12, 3120), (13, 5760), (23, -240), (26, 320), (27, 60), (32, -960), (33, 320), (34, 3680), (37, 1440), (50, -960), (51, 1760), (53, -960), (54, -480), (58, -3360), (59, 640), (70, 720), (71, 720), (72, 1440), (73, 1440), (80, 640), (82, 1440), (115, 640), (132, -720), (133, -720), (143, -480), (160, -480), (184, 2880), (186, 2880), (191, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row209 line 637

Source comment

Selected source equation 381 in the original pair table.

def row209 : Integer.Sparse (Fin 271) := [(0, -6), (1, -205), (2, 175), (3, 2560), (4, 720), (5, -220), (6, 20), (7, 400), (8, 240), (10, -120), (12, 760), (13, 720), (23, -120), (25, -240), (26, 800), (27, 30), (30, -240), (32, -1440), (33, 160), (34, 560), (35, 720), (38, 1440), (50, -480), (51, 240), (53, -1200), (54, -960), (58, -480), (70, 360), (72, 720), (79, -960), (81, 720), (83, 1440), (132, -360), (143, -960), (160, -240), (184, 720), (185, 1440), (187, 1440), (189, 720), (193, 720), (201, 1440), (202, 2880), (218, -720), (219, -480)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row210 line 640

Source comment

Selected source equation 382 in the original pair table.

def row210 : Integer.Sparse (Fin 271) := [(0, 9), (1, -570), (2, 380), (3, 6240), (4, 2400), (5, -400), (6, 45), (7, 1360), (8, 160), (11, 480), (12, 480), (13, 640), (26, 3040), (34, 3040), (36, 1440), (39, 2880), (51, 1280), (54, -1440), (55, -1440), (65, 160), (71, 720), (73, 1440), (79, -1440), (82, 1440), (83, 2880), (133, -720), (143, -2880), (226, 1440), (228, 1440), (232, 5760), (237, 2880), (262, 2880), (263, -960)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row211 line 643

Source comment

Selected source equation 383 in the original pair table.

def row211 : Integer.Sparse (Fin 271) := [(0, -12), (1, -195), (2, 375), (3, 3920), (4, 800), (5, -900), (6, 130), (7, 880), (8, 480), (10, -240), (11, 480), (12, 1120), (13, 1680), (23, -240), (25, -1920), (26, 1280), (27, 60), (30, -960), (32, -960), (34, 2480), (37, 1440), (38, 2880), (50, -1440), (51, 1920), (53, -3120), (55, -480), (58, -960), (70, 720), (72, 1440), (80, 320), (85, 1440), (86, 2880), (110, -1920), (115, 320), (132, -960), (133, -480), (142, -1440), (143, -1440), (147, -480), (179, -480), (186, 1440), (188, 2880), (223, 1440), (229, 1440), (231, 5760), (236, 2880), (245, -1440), (246, -960), (259, 2880)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row212 line 646

Source comment

Selected source equation 384 in the original pair table.

def row212 : Integer.Sparse (Fin 271) := [(0, -13), (1, -150), (2, 375), (3, 3840), (4, 800), (5, -700), (6, 30), (7, 2960), (8, 960), (10, -240), (12, 160), (13, 80), (23, -240), (24, -480), (25, -480), (26, 1760), (27, 60), (34, 3680), (37, 720), (50, -480), (51, 1120), (53, -720), (54, -480), (58, -480), (63, -960), (65, 800), (70, 720), (71, 1440), (79, -1920), (82, 1440), (96, 1440), (132, -240), (143, -480), (159, -480), (191, 1440), (211, 1440), (224, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row213 line 649

Source comment

Selected source equation 385 in the original pair table.

def row213 : Integer.Sparse (Fin 271) := [(0, -9), (1, -280), (2, 565), (3, 7040), (4, 2160), (5, -860), (6, 70), (7, 3120), (8, 800), (11, 640), (12, 80), (13, 160), (26, 3920), (32, -480), (33, 320), (34, 4800), (36, 720), (51, 1920), (55, -240), (65, 640), (71, 720), (79, -2880), (81, 720), (82, 1440), (83, 2880), (133, -240), (143, -4320), (161, -480), (190, 1440), (213, 1440), (215, 1440), (233, 1440), (244, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row214 line 652

Source comment

Selected source equation 386 in the original pair table.

def row214 : Integer.Sparse (Fin 271) := [(0, -12), (1, -20), (2, 615), (3, 4880), (4, 1120), (5, -1320), (6, 175), (7, 1760), (8, 720), (10, -240), (11, 640), (12, 320), (13, 1040), (24, -240), (26, 1840), (27, 60), (30, -480), (32, -480), (34, 3840), (40, 720), (50, -960), (51, 3200), (55, -480), (58, -960), (59, 160), (71, 720), (79, -480), (80, 80), (82, 720), (83, 1440), (91, 1440), (95, 1440), (110, -960), (115, 240), (133, -240), (143, -3120), (147, -480), (179, -480), (186, 720), (188, 1440), (196, 1440), (227, 720), (233, 1440), (239, 1440), (245, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row215 line 655

Source comment

Selected source equation 387 in the original pair table.

def row215 : Integer.Sparse (Fin 271) := [(0, -2), (1, -39), (2, 93), (3, 976), (4, 352), (5, -116), (6, 6), (7, 272), (8, 192), (10, -144), (12, 112), (13, 192), (26, 416), (32, -288), (33, 64), (34, 256), (35, 144), (39, 288), (51, 64), (53, -144), (54, -144), (55, -192), (58, -192), (70, 144), (73, 288), (79, -384), (81, 288), (83, 576), (132, -48), (143, -384), (159, -96), (180, -288), (189, 288), (202, 576), (212, 288), (213, 576), (223, 288), (226, 576), (232, 1152), (248, -192)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row216 line 658

Source comment

Selected source equation 388 in the original pair table.

def row216 : Integer.Sparse (Fin 271) := [(0, -13), (1, 80), (2, 605), (3, 4480), (4, 800), (5, -1220), (6, 170), (7, 1200), (8, 640), (12, 720), (13, 2880), (26, 960), (34, 3040), (37, 720), (39, 1440), (51, 2720), (53, -480), (54, -720), (55, -960), (58, -480), (59, 160), (79, -960), (80, 560), (82, 1440), (83, 2880), (115, 560), (132, -480), (133, -960), (143, -1440), (179, -720), (195, 1440), (201, 2880), (224, 720), (236, 1440), (237, 2880), (249, -960), (258, 1440), (262, 5760)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row217 line 661

Source comment

Selected source equation 389 in the original pair table.

def row217 : Integer.Sparse (Fin 271) := [(0, -5), (1, 76), (2, 127), (3, 656), (5, -216), (6, 24), (7, 384), (8, 128), (10, -48), (12, 112), (13, 512), (23, -48), (27, 12), (34, 720), (50, -96), (51, 544), (53, -192), (58, -240), (59, 160), (61, -192), (70, 144), (71, 288), (79, -192), (80, 32), (90, 288), (115, 112), (132, -96), (133, -96), (147, -96), (157, -96), (169, 288), (179, -96), (207, 288), (224, 288), (227, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row218 line 664

Source comment

Selected source equation 390 in the original pair table.

def row218 : Integer.Sparse (Fin 271) := [(0, -29), (1, 550), (2, 855), (3, 4480), (5, -1500), (6, 190), (7, 1680), (8, 960), (10, -720), (12, 1120), (13, 5120), (31, 320), (34, 3680), (51, 4160), (58, -1920), (59, 640), (70, 720), (71, 1440), (73, 1440), (79, -960), (80, 880), (115, 1680), (132, -720), (133, -2400), (157, -480), (169, 1440), (179, -720), (209, 2880), (224, 720), (227, 2880), (258, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row219 line 667

Source comment

Selected source equation 393 in the original pair table.

def row219 : Integer.Sparse (Fin 271) := [(0, -38), (1, -325), (2, 555), (3, 5040), (5, -820), (6, 30), (7, 2880), (8, 1440), (9, -20), (10, -2160), (12, 2720), (13, 4000), (23, -1440), (27, 360), (34, 1760), (37, 2160), (50, -4320), (53, -4320), (54, -720), (58, -3600), (66, 60), (67, 240), (68, 160), (70, 4320), (72, 4320), (80, 240), (111, -720), (130, -480), (132, -2400), (153, -1440), (168, 2160), (181, -720), (193, 2160), (229, 1440), (246, -720), (248, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row220 line 670

Source comment

Selected source equation 394 in the original pair table.

def row220 : Integer.Sparse (Fin 271) := [(0, -14), (1, -100), (2, 255), (3, 3440), (4, 400), (5, -660), (6, 45), (7, 3040), (8, 640), (10, -240), (12, 640), (13, 960), (24, -240), (26, 960), (27, 60), (33, 160), (34, 3840), (36, 1440), (50, -480), (51, 1520), (54, -480), (58, -480), (59, 320), (65, 160), (71, 720), (79, -480), (81, 1440), (82, 3600), (143, -1200), (160, -480), (184, 1440), (190, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row221 line 673

Source comment

Selected source equation 395 in the original pair table.

def row221 : Integer.Sparse (Fin 271) := [(0, -3), (1, -31), (2, 91), (3, 656), (4, 48), (5, -164), (6, 9), (7, 592), (8, 256), (9, -8), (10, -192), (12, 80), (13, 64), (24, -192), (26, 96), (27, 48), (34, 512), (36, 288), (50, -288), (51, 144), (54, -96), (58, -240), (65, 32), (66, 12), (67, 128), (68, 96), (71, 576), (79, -96), (82, 144), (111, -48), (113, -96), (131, -96), (143, -48), (153, -96), (181, -96), (193, 144), (194, 288), (226, 288), (228, 288), (248, -48)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row222 line 676

Source comment

Selected source equation 396 in the original pair table.

def row222 : Integer.Sparse (Fin 271) := [(0, -12), (1, -195), (2, 775), (3, 6320), (4, 1840), (5, -1040), (6, 70), (7, 2800), (8, 1280), (10, -240), (11, 240), (12, 80), (13, 80), (24, -240), (26, 2880), (27, 60), (30, -240), (32, -960), (33, 160), (34, 3280), (36, 1440), (50, -480), (51, 1760), (54, -480), (58, -480), (65, 160), (71, 720), (79, -3840), (81, 2880), (82, 2880), (83, 4320), (143, -4080), (160, -480), (184, 720), (187, 1440), (190, 1440), (218, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row223 line 679

Source comment

Selected source equation 397 in the original pair table.

def row223 : Integer.Sparse (Fin 271) := [(0, -1), (1, -310), (2, 730), (3, 6400), (4, 2080), (5, -1120), (6, 105), (7, 3040), (8, 960), (11, 560), (26, 3520), (34, 4160), (51, 2240), (52, 1440), (65, 160), (79, -2880), (81, 1440), (82, 3600), (83, 4320), (143, -4800), (243, 1440), (244, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row224 line 682

Source comment

Selected source equation 398 in the original pair table.

def row224 : Integer.Sparse (Fin 271) := [(0, -14), (1, -15), (2, 45), (3, 2320), (5, -440), (6, 70), (7, 1680), (8, 640), (9, -60), (10, -480), (23, -480), (25, -240), (26, 640), (27, 120), (34, 2480), (35, 720), (51, 480), (53, -1200), (54, -240), (63, -480), (65, 400), (66, 60), (67, 800), (68, 400), (70, 1440), (81, 1440), (112, -720), (113, -480), (132, -480), (143, -960), (154, -480), (159, -480), (171, 720), (181, -240), (189, 1440), (211, 720), (219, -240), (223, 720), (226, 1440), (248, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row225 line 685

Source comment

Selected source equation 399 in the original pair table.

def row225 : Integer.Sparse (Fin 271) := [(0, -3), (1, 15), (2, 108), (3, 768), (4, 144), (5, -196), (6, 20), (7, 480), (8, 176), (11, 16), (12, 32), (13, 112), (26, 272), (33, 32), (34, 768), (36, 144), (51, 480), (55, -48), (58, -48), (59, 32), (65, 64), (71, 288), (79, -384), (81, 144), (82, 432), (115, 16), (133, -96), (143, -288), (161, -96), (190, 288), (213, 144), (215, 144), (233, 144), (244, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row226 line 688

Source comment

Selected source equation 400 in the original pair table.

def row226 : Integer.Sparse (Fin 271) := [(0, -33), (1, 235), (2, 950), (3, 4480), (4, 160), (5, -1600), (6, 100), (7, 3680), (8, 2240), (10, -2400), (12, 1360), (13, 2560), (26, 160), (32, -480), (33, 160), (34, 3440), (37, 720), (51, 2240), (53, -240), (58, -3840), (59, 160), (70, 1440), (71, 2880), (72, 1440), (73, 2880), (79, -1440), (80, 320), (82, 1440), (115, 400), (132, -720), (133, -960), (143, -480), (159, -480), (180, -720), (191, 1440), (212, 720), (213, 1440), (224, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row227 line 691

Source comment

Selected source equation 401 in the original pair table.

def row227 : Integer.Sparse (Fin 271) := [(0, -29), (1, -45), (2, 1290), (3, 6720), (4, 960), (5, -1080), (6, 60), (7, 1680), (8, 1440), (10, -720), (12, 2160), (13, 4400), (30, -720), (32, -1440), (34, 1680), (41, 4320), (50, -2880), (51, 3120), (58, -2880), (59, 480), (79, -1440), (80, 240), (84, 4320), (115, 960), (184, 2160), (198, 4320), (200, 4320), (218, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row228 line 694

Source comment

Selected source equation 402 in the original pair table.

def row228 : Integer.Sparse (Fin 271) := [(0, 3), (1, -230), (2, 1095), (3, 6480), (4, 1520), (5, -1720), (6, 150), (7, 3040), (8, 1760), (11, 240), (26, 2560), (34, 4000), (51, 2640), (56, 1440), (65, 800), (79, -3360), (84, 2880), (143, -720), (215, 1440), (269, 4320)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row229 line 697

Source comment

Selected source equation 403 in the original pair table.

def row229 : Integer.Sparse (Fin 271) := [(0, -16), (1, 140), (2, 1155), (3, 4000), (4, 880), (5, -1820), (6, 95), (7, 3760), (8, 3040), (12, 80), (13, 160), (26, 1120), (30, -960), (32, -960), (34, 2480), (41, 1440), (50, -960), (51, 1120), (55, -240), (58, -960), (65, 480), (74, 1440), (79, -2400), (84, 1440), (89, 720), (99, 1440), (133, -240), (148, -720), (180, -720), (198, 2880), (211, 720), (213, 1440), (230, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row230 line 700

Source comment

Selected source equation 404 in the original pair table.

def row230 : Integer.Sparse (Fin 271) := [(0, -1), (1, 64), (2, 143), (3, 304), (4, 32), (5, -412), (6, 60), (7, 48), (8, 256), (9, -4), (11, 32), (12, 16), (25, -96), (26, 64), (30, -192), (32, -192), (34, 288), (38, 288), (51, 608), (53, -96), (67, 16), (69, 64), (85, 144), (110, -192), (142, -48), (143, -96), (147, -144), (149, 288), (179, -144), (188, 576), (223, 144), (231, 288), (245, -192), (246, -48), (258, 288), (259, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row231 line 703

Source comment

Selected source equation 405 in the original pair table.

def row231 : Integer.Sparse (Fin 271) := [(0, -27), (1, 505), (2, 1080), (3, 3840), (5, -2140), (6, 250), (7, 2160), (8, 1920), (9, -20), (12, 560), (13, 2640), (34, 3680), (50, -480), (51, 4080), (53, -240), (58, -1200), (59, 720), (67, 160), (69, 560), (80, 400), (84, 1440), (115, 800), (132, -240), (133, -960), (154, -480), (155, -480), (173, 720), (182, -720), (199, 1440), (200, 1440), (207, 720), (219, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row232 line 706

Source comment

Selected source equation 406 in the original pair table.

def row232 : Integer.Sparse (Fin 271) := [(0, -29), (1, 535), (2, 1010), (3, 3600), (4, 160), (5, -2000), (6, 240), (7, 1600), (8, 1600), (12, 560), (13, 2720), (26, 80), (34, 3120), (41, 720), (50, -480), (51, 4240), (55, -480), (58, -1920), (59, 800), (74, 720), (80, 240), (84, 720), (94, 720), (95, 720), (115, 880), (133, -960), (200, 1440), (207, 720), (209, 720), (230, 1440), (264, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row233 line 709

Source comment

Selected source equation 407 in the original pair table.

def row233 : Integer.Sparse (Fin 271) := [(0, -21), (1, 275), (2, 450), (3, 1440), (4, 160), (5, -1240), (6, 200), (7, 640), (8, 1040), (9, -20), (11, 160), (12, 160), (13, 720), (25, -240), (26, 320), (34, 1360), (38, 720), (50, -480), (51, 2000), (53, -480), (55, -480), (58, -480), (67, 80), (69, 320), (72, 720), (80, 160), (86, 720), (110, -480), (115, 400), (132, -240), (133, -480), (142, -240), (143, -480), (188, 1440), (231, 2160), (236, 720), (245, -480), (246, -240), (259, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row234 line 712

Source comment

Selected source equation 408 in the original pair table.

def row234 : Integer.Sparse (Fin 271) := [(0, -23), (1, -105), (2, 1130), (3, 5680), (4, 1200), (5, -1300), (6, 90), (7, 1760), (8, 2000), (10, -240), (12, 1600), (13, 2800), (24, -240), (26, 480), (27, 60), (30, -720), (32, -1920), (33, 320), (34, 1040), (38, 1440), (41, 1440), (50, -3120), (51, 1920), (54, -480), (55, -960), (58, -2400), (59, 320), (72, 720), (74, 1440), (79, -960), (83, 1440), (84, 1440), (115, 480), (133, -720), (143, -480), (160, -480), (184, 2160), (187, 1440), (188, 2880), (192, 1440), (198, 2880), (200, 1440), (218, -720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row235 line 715

Source comment

Selected source equation 409 in the original pair table.

def row235 : Integer.Sparse (Fin 271) := [(0, -14), (1, 15), (2, 500), (3, 3840), (4, 960), (5, -1260), (6, 175), (7, 480), (8, 960), (9, -20), (12, 960), (13, 2880), (24, -480), (26, 800), (27, 120), (30, -480), (32, -960), (34, 2080), (38, 1440), (41, 1440), (50, -960), (51, 2080), (53, -960), (54, -480), (55, -2400), (66, 60), (67, 80), (69, 320), (80, 640), (91, 1440), (110, -480), (111, -240), (113, -480), (115, 640), (131, -480), (132, -480), (133, -960), (147, -480), (153, -480), (155, -960), (170, 720), (172, 1440), (179, -960), (181, -480), (182, -240), (185, 720), (188, 1440), (200, 1440), (201, 1440), (225, 2880), (230, 1440), (245, -720), (249, -240), (259, 1440), (263, -720), (264, 2880)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row236 line 718

Source comment

Selected source equation 410 in the original pair table.

def row236 : Integer.Sparse (Fin 271) := [(0, -2), (1, 11), (2, 115), (3, 424), (4, 64), (5, -170), (6, 8), (7, 384), (8, 296), (12, 32), (13, 40), (25, -24), (26, 104), (30, -48), (32, -72), (33, 16), (34, 232), (38, 72), (50, -48), (51, 80), (53, -48), (58, -48), (63, -48), (65, 40), (72, 72), (79, -240), (83, 144), (84, 144), (92, 72), (99, 144), (132, -24), (143, -48), (148, -72), (159, -48), (180, -72), (192, 144), (198, 144), (211, 72), (212, 72), (213, 144), (225, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row237 line 721

Source comment

Selected source equation 412 in the original pair table.

def row237 : Integer.Sparse (Fin 271) := [(0, -6), (1, 72), (2, 193), (3, 624), (4, 80), (5, -340), (6, 31), (7, 448), (8, 384), (11, 32), (12, 16), (13, 64), (26, 176), (32, -96), (34, 384), (51, 368), (58, -48), (65, 32), (73, 144), (79, -288), (83, 432), (84, 288), (115, 16), (133, -48), (143, -288), (213, 288), (233, 144), (258, 144), (269, 144)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row238 line 724

Source comment

Selected source equation 419 in the original pair table.

def row238 : Integer.Sparse (Fin 271) := [(0, 27), (1, -905), (2, 610), (3, 2960), (4, 2000), (5, -400), (6, 20), (7, 240), (8, 560), (9, -20), (12, 560), (23, -240), (24, -1680), (26, 160), (27, 900), (30, -2400), (46, 720), (50, -5040), (51, 400), (55, -960), (66, 180), (67, 80), (69, 80), (111, -240), (113, -1440), (136, 720), (137, 1440), (139, 1440), (148, -960), (155, -480), (181, -240), (182, -240), (234, 720), (256, 720), (257, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row239 line 727

Source comment

Selected source equation 422 in the original pair table.

def row239 : Integer.Sparse (Fin 271) := [(0, 33), (1, -685), (2, 305), (3, 6480), (4, 2720), (5, -380), (6, 45), (7, 1120), (8, 80), (12, 400), (13, 400), (24, -240), (26, 3360), (30, -720), (32, -480), (33, 640), (34, 2000), (43, 1440), (51, 1040), (65, 640), (79, -960), (88, 720), (91, 1440), (107, 1440), (214, 1440), (215, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row240 line 730

Source comment

Selected source equation 423 in the original pair table.

def row240 : Integer.Sparse (Fin 271) := [(0, -3), (1, -39), (2, 91), (3, 768), (4, 192), (5, -68), (6, 5), (7, 144), (8, 64), (12, 176), (13, 176), (25, -192), (26, 256), (30, -144), (32, -672), (33, 64), (34, 224), (42, 288), (50, -48), (51, 160), (58, -192), (63, -144), (65, 64), (79, -192), (88, 144), (95, 288), (96, 288), (101, 144), (102, 288), (133, -48), (180, -144), (211, 144), (213, 288), (216, 288)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row241 line 733

Source comment

Selected source equation 425 in the original pair table.

def row241 : Integer.Sparse (Fin 271) := [(0, -11), (1, -790), (2, 850), (3, 5920), (4, 1280), (5, -520), (6, 35), (7, 640), (8, 320), (9, -20), (12, 2000), (13, 1440), (23, -1200), (25, -2880), (26, 480), (27, 720), (30, -3840), (32, -3840), (34, 400), (50, -5760), (51, 800), (53, -960), (54, -2160), (63, -2880), (66, 180), (67, 80), (68, 80), (111, -240), (112, -960), (113, -480), (120, 720), (122, 2880), (125, 1440), (148, -1920), (154, -480), (182, -480), (206, 1440), (234, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row242 line 736

Source comment

Selected source equation 430 in the original pair table.

def row242 : Integer.Sparse (Fin 271) := [(0, -21), (1, 80), (2, 365), (3, 4080), (5, -900), (6, 170), (7, 560), (9, -60), (12, 1200), (13, 4160), (23, -960), (25, -960), (27, 240), (30, -960), (32, -1920), (34, 1760), (51, 2240), (53, -1440), (62, -2640), (66, 180), (67, 240), (68, 160), (110, -960), (111, -240), (112, -480), (113, -480), (116, 720), (124, 1440), (130, -720), (145, 1440), (147, -1920), (179, -720), (223, 720), (245, -960), (246, -240), (258, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row243 line 739

Source comment

Selected source equation 433 in the original pair table.

def row243 : Integer.Sparse (Fin 271) := [(0, -26), (1, -335), (2, 380), (3, 3600), (4, 160), (5, -320), (6, 5), (7, 1040), (8, 480), (9, -20), (10, -960), (12, 1920), (13, 1920), (23, -1200), (24, -480), (27, 660), (34, 160), (37, 720), (46, 1440), (50, -3120), (51, 80), (53, -480), (54, -1680), (58, -1200), (66, 120), (67, 160), (111, -720), (112, -480), (113, -240), (120, 1440), (136, 720), (153, -480), (181, -480), (193, 720), (234, 1440), (235, 1440), (248, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row244 line 742

Source comment

Selected source equation 434 in the original pair table.

def row244 : Integer.Sparse (Fin 271) := [(0, -9), (1, -10), (2, -35), (3, 3040), (4, 800), (5, -320), (6, 40), (7, 2240), (8, 320), (9, -20), (12, 320), (13, 80), (23, -480), (25, -2160), (26, 1440), (32, -480), (34, 960), (37, 720), (50, -480), (51, 160), (53, -2640), (63, -960), (67, 240), (89, 2880), (111, -480), (143, -960), (154, -480), (193, 720), (206, 1440), (219, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row245 line 745

Source comment

Selected source equation 436 in the original pair table.

def row245 : Integer.Sparse (Fin 271) := [(0, 6), (1, -240), (2, 565), (3, 4160), (4, 1680), (5, -480), (6, 35), (7, 800), (8, 880), (9, -20), (24, -240), (26, 1520), (27, 60), (30, -480), (34, 320), (36, 720), (45, 1440), (50, -1440), (51, 800), (55, -1680), (67, 160), (69, 80), (79, -1200), (99, 1440), (111, -240), (113, -240), (143, -960), (155, -480), (226, 720), (250, 1440), (255, 1440), (257, 1440), (263, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row246 line 748

Source comment

Selected source equation 444 in the original pair table.

def row246 : Integer.Sparse (Fin 271) := [(0, 1), (1, -490), (2, 640), (3, 3520), (4, 720), (5, -740), (6, 65), (7, 880), (8, 1120), (9, -40), (10, -480), (11, 80), (12, 800), (13, 720), (23, -480), (24, -240), (26, 480), (27, 420), (29, -240), (30, -720), (34, 560), (39, 720), (42, 720), (50, -2160), (51, 800), (54, -1200), (66, 120), (67, 160), (69, 240), (88, 1440), (112, -480), (113, -960), (126, 1440), (138, 720), (146, -480), (147, -240), (148, -240), (181, -240), (232, 720), (234, 720), (240, 720), (248, -240), (253, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row247 line 751

Source comment

Selected source equation 445 in the original pair table.

def row247 : Integer.Sparse (Fin 271) := [(0, -14), (1, -145), (2, 360), (3, 4400), (4, 640), (5, -760), (6, 115), (7, 1120), (8, 240), (9, -20), (12, 560), (13, 2640), (25, -240), (26, 1360), (33, 560), (34, 2320), (38, 720), (51, 2480), (53, -1440), (59, 560), (63, -480), (67, 160), (69, 80), (80, 80), (91, 1440), (95, 1440), (106, 720), (113, -480), (115, 400), (143, -480), (154, -480), (201, 720), (207, 720), (210, 1440), (219, -240)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row248 line 754

Source comment

Selected source equation 446 in the original pair table.

def row248 : Integer.Sparse (Fin 271) := [(0, 3), (1, -80), (2, 51), (3, 608), (4, 232), (5, -60), (6, 6), (7, 80), (8, 72), (11, 24), (12, 64), (13, 64), (26, 240), (27, 6), (30, -72), (34, 144), (42, 72), (44, 72), (50, -120), (51, 64), (55, -96), (56, 72), (79, -48), (99, 216), (135, 144), (143, -48), (147, -24), (148, -72), (240, 72), (255, 144), (269, 72), (270, 72)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row249 line 757

Source comment

Selected source equation 447 in the original pair table.

def row249 : Integer.Sparse (Fin 271) := [(0, -29), (1, -5), (2, 660), (3, 5920), (4, 560), (5, -800), (6, 110), (7, 480), (8, 240), (12, 1840), (13, 5520), (26, 880), (32, -480), (33, 640), (34, 2320), (41, 720), (50, -240), (51, 3120), (58, -960), (59, 640), (80, 240), (90, 1440), (91, 720), (94, 1440), (95, 720), (106, 720), (108, 720), (115, 800), (133, -480), (147, -240), (200, 720), (207, 720), (208, 1440), (209, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row250 line 760

Source comment

Selected source equation 448 in the original pair table.

def row250 : Integer.Sparse (Fin 271) := [(0, -36), (1, 35), (2, 615), (3, 3440), (5, -860), (6, 100), (7, 560), (8, 800), (9, -20), (12, 1200), (13, 3360), (32, -960), (34, 640), (37, 720), (50, -1440), (51, 1840), (53, -1200), (58, -1440), (67, 80), (69, 160), (80, 160), (94, 1440), (113, -480), (115, 400), (132, -480), (147, -480), (153, -480), (235, 1440), (236, 720), (245, -480), (246, -240), (254, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row251 line 763

Source comment

Selected source equation 454 in the original pair table.

def row251 : Integer.Sparse (Fin 271) := [(0, -18), (1, -455), (2, 160), (3, 7200), (4, 1520), (5, -260), (6, 45), (11, 80), (12, 1280), (13, 3680), (26, 3120), (33, 2400), (34, 1920), (40, 720), (51, 880), (54, -480), (55, -720), (59, 720), (80, 80), (115, 160), (119, 1440), (128, 1440), (135, 1440), (148, -480), (196, 720), (208, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row252 line 766

Source comment

Selected source equation 455 in the original pair table.

def row252 : Integer.Sparse (Fin 271) := [(0, -38), (1, -205), (2, 240), (3, 5840), (4, 160), (5, -560), (6, 75), (7, 640), (8, 160), (9, -20), (12, 1360), (13, 4160), (23, -240), (26, 2240), (27, 180), (33, 1920), (34, 2320), (37, 720), (50, -1440), (51, 1280), (53, -480), (54, -1200), (59, 560), (63, -1440), (66, 120), (68, 80), (69, 80), (80, 320), (112, -480), (115, 400), (118, 1440), (119, 1440), (126, 720), (131, -720), (146, -240), (148, -960), (154, -480), (182, -480), (195, 720), (210, 1440), (249, -240), (265, 1440)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row253 line 769

Source comment

Selected source equation 460 in the original pair table.

def row253 : Integer.Sparse (Fin 271) := [(0, -3), (1, -280), (2, 45), (3, 3440), (4, 1000), (5, -210), (6, 30), (7, 280), (8, 120), (11, 160), (12, 80), (13, 800), (26, 2200), (33, 960), (34, 1240), (50, -120), (51, 200), (52, 360), (54, -360), (55, -480), (63, -720), (65, 360), (99, 360), (119, 720), (128, 720), (143, -120), (148, -480), (214, 720), (240, 360), (243, 360), (270, 360)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.row254 line 772

Source comment

Selected source equation 461 in the original pair table.

def row254 : Integer.Sparse (Fin 271) := [(0, -22), (1, -190), (2, 355), (3, 5680), (4, 800), (5, -620), (6, 95), (7, 1280), (8, 240), (9, -40), (11, 80), (12, 480), (13, 2400), (24, -240), (26, 3040), (27, 120), (30, -240), (32, -480), (33, 1520), (34, 2400), (36, 720), (50, -1440), (51, 1120), (54, -960), (63, -2400), (65, 560), (66, 120), (67, 160), (68, 240), (112, -1200), (113, -240), (118, 1440), (119, 1440), (126, 720), (131, -480), (135, 720), (147, -240), (148, -1200), (180, -480), (182, -240), (216, 1440), (228, 720), (238, 720), (240, 720), (248, -240), (251, 720)]

Mentions: OAI.MUB6.Certificate.Integer.Sparse

def OAI.MUB6.Certificate.PairData.rows line 774
def OAI.MUB6.Certificate.PairData.denominator line 776
theorem OAI.MUB6.Certificate.PairData.denominator_pos line 778
def OAI.MUB6.Certificate.PairData.combination0 line 780
def OAI.MUB6.Certificate.PairData.target0 line 782
def OAI.MUB6.Certificate.PairData.combination1 line 784
def OAI.MUB6.Certificate.PairData.target1 line 786