FS002M · theorem body

four_square_euler_add_permute_sixteen

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

All sixteen Hamilton diagonal squares transpose from coordinate order into row-major norm order.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

forall u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15. ((((((u0) + ((((u1) + (u2)) + (u3))))) + (((((u4) + (u5)) + (u6)) + (u7)))) + ((((((u8) + (u9)) + (u10)) + (u11))) + (((((u12) + (u13)) + (u14)) + (u15)))))) = (((((((((u0) + (u4)) + (u8)) + (u12))) + (((((u5) + (u1)) + (u13)) + (u11)))) + (((((u9) + (u15)) + (u2)) + (u6)))) + (((((u14) + (u10)) + (u7)) + (u3)))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

none

In local proof propositions

none
Exact expanded first-order statement
forall u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15. ((((((u0) + ((((u1) + (u2)) + (u3))))) + (((((u4) + (u5)) + (u6)) + (u7)))) + ((((((u8) + (u9)) + (u10)) + (u11))) + (((((u12) + (u13)) + (u14)) + (u15)))))) = (((((((((u0) + (u4)) + (u8)) + (u12))) + (((((u5) + (u1)) + (u13)) + (u11)))) + (((((u9) + (u15)) + (u2)) + (u6)))) + (((((u14) + (u10)) + (u7)) + (u3)))))

Proof neighborhood

Direct theorem prerequisites

add_assoc · Stable closed add_comm · Stable closed FS0006 four_square_add_swap_right_tail

Direct theorem dependents

FS002T four_square_euler_diagonal_regroup

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

232 script commands · 36 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
four square add swap right tail
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro u0
  2. L2
    intro u1
  3. L3
    intro u2
  4. L4
    intro u3
  5. L5
    intro u4
  6. L6
    intro u5
  7. L7
    intro u6
  8. L8
    intro u7
  9. L9
    intro u8
  10. L10
    intro u9
02Fix variables and assumptionsL11–16

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro u10
  2. L12
    intro u11
  3. L13
    intro u12
  4. L14
    intro u13
  5. L15
    intro u14
  6. L16
    intro u15
03Calculate and transport equalitiesL17–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L17
    trans ((u0) + ((u1) + ((u2) + ((u3) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))))
  2. L18
    simp [add_assoc]
  3. L19
    trans ((u0) + ((u4) + ((u8) + ((u12) + ((u5) + ((u1) + ((u13) + ((u11) + ((u9) + ((u15) + ((u2) + ((u6) + ((u14) + ((u10) + ((u7) + (u3))))))))))))))))
  4. L20
    congr
  5. L21
    refl
  6. L22
    trans ((u4) + ((u1) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))))))
  7. L23
    trans ((u1) + ((u4) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))))))
  8. L24
    congr
  9. L25
    refl
  10. L26
    trans ((u2) + ((u4) + ((u3) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))
04Calculate and transport equalitiesL27–28

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    congr
  2. L28
    refl
05Use earlier factsL29–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    apply four_square_add_swap_right_tail
  2. L30
    apply four_square_add_swap_right_tail
  3. L31
    apply four_square_add_swap_right_tail
06Calculate and transport equalitiesL32–41

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    congr
  2. L33
    refl
  3. L34
    trans ((u8) + ((u1) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))
  4. L35
    trans ((u1) + ((u8) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))
  5. L36
    congr
  6. L37
    refl
  7. L38
    trans ((u2) + ((u8) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))))
  8. L39
    congr
  9. L40
    refl
  10. L41
    trans ((u3) + ((u8) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))
07Calculate and transport equalitiesL42–49

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    congr
  2. L43
    refl
  3. L44
    trans ((u5) + ((u8) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))
  4. L45
    congr
  5. L46
    refl
  6. L47
    trans ((u6) + ((u8) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))
  7. L48
    congr
  8. L49
    refl
08Use earlier factsL50–55

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    apply four_square_add_swap_right_tail
  2. L51
    apply four_square_add_swap_right_tail
  3. L52
    apply four_square_add_swap_right_tail
  4. L53
    apply four_square_add_swap_right_tail
  5. L54
    apply four_square_add_swap_right_tail
  6. L55
    apply four_square_add_swap_right_tail
09Calculate and transport equalitiesL56–65

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L56
    congr
  2. L57
    refl
  3. L58
    trans ((u12) + ((u1) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))))
  4. L59
    trans ((u1) + ((u12) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))))
  5. L60
    congr
  6. L61
    refl
  7. L62
    trans ((u2) + ((u12) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))))
  8. L63
    congr
  9. L64
    refl
  10. L65
    trans ((u3) + ((u12) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))
10Calculate and transport equalitiesL66–75

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L66
    congr
  2. L67
    refl
  3. L68
    trans ((u5) + ((u12) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))
  4. L69
    congr
  5. L70
    refl
  6. L71
    trans ((u6) + ((u12) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))
  7. L72
    congr
  8. L73
    refl
  9. L74
    trans ((u7) + ((u12) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))
  10. L75
    congr
11Calculate and transport equalitiesL76–82

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L76
    refl
  2. L77
    trans ((u9) + ((u12) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))
  3. L78
    congr
  4. L79
    refl
  5. L80
    trans ((u10) + ((u12) + ((u11) + ((u13) + ((u14) + (u15))))))
  6. L81
    congr
  7. L82
    refl
12Use earlier factsL83–91

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L83
    apply four_square_add_swap_right_tail
  2. L84
    apply four_square_add_swap_right_tail
  3. L85
    apply four_square_add_swap_right_tail
  4. L86
    apply four_square_add_swap_right_tail
  5. L87
    apply four_square_add_swap_right_tail
  6. L88
    apply four_square_add_swap_right_tail
  7. L89
    apply four_square_add_swap_right_tail
  8. L90
    apply four_square_add_swap_right_tail
  9. L91
    apply four_square_add_swap_right_tail
13Calculate and transport equalitiesL92–100

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L92
    congr
  2. L93
    refl
  3. L94
    trans ((u5) + ((u1) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))))
  4. L95
    trans ((u1) + ((u5) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))))
  5. L96
    congr
  6. L97
    refl
  7. L98
    trans ((u2) + ((u5) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))
  8. L99
    congr
  9. L100
    refl
14Use earlier factsL101–103

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L101
    apply four_square_add_swap_right_tail
  2. L102
    apply four_square_add_swap_right_tail
  3. L103
    apply four_square_add_swap_right_tail
15Calculate and transport equalitiesL104–113

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L104
    congr
  2. L105
    refl
  3. L106
    congr
  4. L107
    refl
  5. L108
    trans ((u13) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15))))))))))
  6. L109
    trans ((u2) + ((u13) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15))))))))))
  7. L110
    congr
  8. L111
    refl
  9. L112
    trans ((u3) + ((u13) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15)))))))))
  10. L113
    congr
16Calculate and transport equalitiesL114–123

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L114
    refl
  2. L115
    trans ((u6) + ((u13) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15))))))))
  3. L116
    congr
  4. L117
    refl
  5. L118
    trans ((u7) + ((u13) + ((u9) + ((u10) + ((u11) + ((u14) + (u15)))))))
  6. L119
    congr
  7. L120
    refl
  8. L121
    trans ((u9) + ((u13) + ((u10) + ((u11) + ((u14) + (u15))))))
  9. L122
    congr
  10. L123
    refl
17Calculate and transport equalitiesL124–126

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L124
    trans ((u10) + ((u13) + ((u11) + ((u14) + (u15)))))
  2. L125
    congr
  3. L126
    refl
18Use earlier factsL127–133

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L127
    apply four_square_add_swap_right_tail
  2. L128
    apply four_square_add_swap_right_tail
  3. L129
    apply four_square_add_swap_right_tail
  4. L130
    apply four_square_add_swap_right_tail
  5. L131
    apply four_square_add_swap_right_tail
  6. L132
    apply four_square_add_swap_right_tail
  7. L133
    apply four_square_add_swap_right_tail
19Calculate and transport equalitiesL134–143

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L134
    congr
  2. L135
    refl
  3. L136
    trans ((u11) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u14) + (u15)))))))))
  4. L137
    trans ((u2) + ((u11) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u14) + (u15)))))))))
  5. L138
    congr
  6. L139
    refl
  7. L140
    trans ((u3) + ((u11) + ((u6) + ((u7) + ((u9) + ((u10) + ((u14) + (u15))))))))
  8. L141
    congr
  9. L142
    refl
  10. L143
    trans ((u6) + ((u11) + ((u7) + ((u9) + ((u10) + ((u14) + (u15)))))))
20Calculate and transport equalitiesL144–151

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L144
    congr
  2. L145
    refl
  3. L146
    trans ((u7) + ((u11) + ((u9) + ((u10) + ((u14) + (u15))))))
  4. L147
    congr
  5. L148
    refl
  6. L149
    trans ((u9) + ((u11) + ((u10) + ((u14) + (u15)))))
  7. L150
    congr
  8. L151
    refl
21Use earlier factsL152–157

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L152
    apply four_square_add_swap_right_tail
  2. L153
    apply four_square_add_swap_right_tail
  3. L154
    apply four_square_add_swap_right_tail
  4. L155
    apply four_square_add_swap_right_tail
  5. L156
    apply four_square_add_swap_right_tail
  6. L157
    apply four_square_add_swap_right_tail
22Calculate and transport equalitiesL158–167

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L158
    congr
  2. L159
    refl
  3. L160
    trans ((u9) + ((u2) + ((u3) + ((u6) + ((u7) + ((u10) + ((u14) + (u15))))))))
  4. L161
    trans ((u2) + ((u9) + ((u3) + ((u6) + ((u7) + ((u10) + ((u14) + (u15))))))))
  5. L162
    congr
  6. L163
    refl
  7. L164
    trans ((u3) + ((u9) + ((u6) + ((u7) + ((u10) + ((u14) + (u15)))))))
  8. L165
    congr
  9. L166
    refl
  10. L167
    trans ((u6) + ((u9) + ((u7) + ((u10) + ((u14) + (u15))))))
23Calculate and transport equalitiesL168–169

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L168
    congr
  2. L169
    refl
24Use earlier factsL170–173

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L170
    apply four_square_add_swap_right_tail
  2. L171
    apply four_square_add_swap_right_tail
  3. L172
    apply four_square_add_swap_right_tail
  4. L173
    apply four_square_add_swap_right_tail
25Calculate and transport equalitiesL174–183

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L174
    congr
  2. L175
    refl
  3. L176
    trans ((u15) + ((u2) + ((u3) + ((u6) + ((u7) + ((u10) + (u14)))))))
  4. L177
    trans ((u2) + ((u15) + ((u3) + ((u6) + ((u7) + ((u10) + (u14)))))))
  5. L178
    congr
  6. L179
    refl
  7. L180
    trans ((u3) + ((u15) + ((u6) + ((u7) + ((u10) + (u14))))))
  8. L181
    congr
  9. L182
    refl
  10. L183
    trans ((u6) + ((u15) + ((u7) + ((u10) + (u14)))))
26Calculate and transport equalitiesL184–191

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L184
    congr
  2. L185
    refl
  3. L186
    trans ((u7) + ((u15) + ((u10) + (u14))))
  4. L187
    congr
  5. L188
    refl
  6. L189
    trans ((u10) + ((u15) + (u14)))
  7. L190
    congr
  8. L191
    refl
27Use earlier factsL192–197

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L192
    apply add_comm
  2. L193
    apply four_square_add_swap_right_tail
  3. L194
    apply four_square_add_swap_right_tail
  4. L195
    apply four_square_add_swap_right_tail
  5. L196
    apply four_square_add_swap_right_tail
  6. L197
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL198–202

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L198
    congr
  2. L199
    refl
  3. L200
    congr
  4. L201
    refl
  5. L202
    trans ((u6) + ((u3) + ((u7) + ((u10) + (u14)))))
29Use earlier factsL203–203

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L203
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL204–212

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L204
    congr
  2. L205
    refl
  3. L206
    trans ((u14) + ((u3) + ((u7) + (u10))))
  4. L207
    trans ((u3) + ((u14) + ((u7) + (u10))))
  5. L208
    congr
  6. L209
    refl
  7. L210
    trans ((u7) + ((u14) + (u10)))
  8. L211
    congr
  9. L212
    refl
31Use earlier factsL213–215

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L213
    apply add_comm
  2. L214
    apply four_square_add_swap_right_tail
  3. L215
    apply four_square_add_swap_right_tail
32Calculate and transport equalitiesL216–221

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L216
    congr
  2. L217
    refl
  3. L218
    trans ((u10) + ((u3) + (u7)))
  4. L219
    trans ((u3) + ((u10) + (u7)))
  5. L220
    congr
  6. L221
    refl
33Use earlier factsL222–223

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L222
    apply add_comm
  2. L223
    apply four_square_add_swap_right_tail
34Calculate and transport equalitiesL224–226

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L224
    congr
  2. L225
    refl
  3. L226
    trans ((u7) + (u3))
35Use earlier factsL227–227

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L227
    apply add_comm
36Calculate and transport equalitiesL228–232

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L228
    congr
  2. L229
    refl
  3. L230
    refl
  4. L231
    symm
  5. L232
    simp [add_assoc]

Library-wide reading audit

Original defined command ledger · 232 lines
  1. 0001intro u0
  2. 0002intro u1
  3. 0003intro u2
  4. 0004intro u3
  5. 0005intro u4
  6. 0006intro u5
  7. 0007intro u6
  8. 0008intro u7
  9. 0009intro u8
  10. 0010intro u9
  11. 0011intro u10
  12. 0012intro u11
  13. 0013intro u12
  14. 0014intro u13
  15. 0015intro u14
  16. 0016intro u15
  17. 0017trans ((u0) + ((u1) + ((u2) + ((u3) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))))
  18. 0018simp [add_assoc]
  19. 0019trans ((u0) + ((u4) + ((u8) + ((u12) + ((u5) + ((u1) + ((u13) + ((u11) + ((u9) + ((u15) + ((u2) + ((u6) + ((u14) + ((u10) + ((u7) + (u3))))))))))))))))
  20. 0020congr
  21. 0021refl
  22. 0022trans ((u4) + ((u1) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))))))
  23. 0023trans ((u1) + ((u4) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))))))
  24. 0024congr
  25. 0025refl
  26. 0026trans ((u2) + ((u4) + ((u3) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))
  27. 0027congr
  28. 0028refl
  29. 0029apply four_square_add_swap_right_tail
  30. 0030apply four_square_add_swap_right_tail
  31. 0031apply four_square_add_swap_right_tail
  32. 0032congr
  33. 0033refl
  34. 0034trans ((u8) + ((u1) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))
  35. 0035trans ((u1) + ((u8) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))))
  36. 0036congr
  37. 0037refl
  38. 0038trans ((u2) + ((u8) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))))
  39. 0039congr
  40. 0040refl
  41. 0041trans ((u3) + ((u8) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))))
  42. 0042congr
  43. 0043refl
  44. 0044trans ((u5) + ((u8) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15)))))))))))
  45. 0045congr
  46. 0046refl
  47. 0047trans ((u6) + ((u8) + ((u7) + ((u9) + ((u10) + ((u11) + ((u12) + ((u13) + ((u14) + (u15))))))))))
  48. 0048congr
  49. 0049refl
  50. 0050apply four_square_add_swap_right_tail
  51. 0051apply four_square_add_swap_right_tail
  52. 0052apply four_square_add_swap_right_tail
  53. 0053apply four_square_add_swap_right_tail
  54. 0054apply four_square_add_swap_right_tail
  55. 0055apply four_square_add_swap_right_tail
  56. 0056congr
  57. 0057refl
  58. 0058trans ((u12) + ((u1) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))))
  59. 0059trans ((u1) + ((u12) + ((u2) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))))
  60. 0060congr
  61. 0061refl
  62. 0062trans ((u2) + ((u12) + ((u3) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))))
  63. 0063congr
  64. 0064refl
  65. 0065trans ((u3) + ((u12) + ((u5) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))
  66. 0066congr
  67. 0067refl
  68. 0068trans ((u5) + ((u12) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))
  69. 0069congr
  70. 0070refl
  71. 0071trans ((u6) + ((u12) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))
  72. 0072congr
  73. 0073refl
  74. 0074trans ((u7) + ((u12) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))
  75. 0075congr
  76. 0076refl
  77. 0077trans ((u9) + ((u12) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))
  78. 0078congr
  79. 0079refl
  80. 0080trans ((u10) + ((u12) + ((u11) + ((u13) + ((u14) + (u15))))))
  81. 0081congr
  82. 0082refl
  83. 0083apply four_square_add_swap_right_tail
  84. 0084apply four_square_add_swap_right_tail
  85. 0085apply four_square_add_swap_right_tail
  86. 0086apply four_square_add_swap_right_tail
  87. 0087apply four_square_add_swap_right_tail
  88. 0088apply four_square_add_swap_right_tail
  89. 0089apply four_square_add_swap_right_tail
  90. 0090apply four_square_add_swap_right_tail
  91. 0091apply four_square_add_swap_right_tail
  92. 0092congr
  93. 0093refl
  94. 0094trans ((u5) + ((u1) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))))
  95. 0095trans ((u1) + ((u5) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15))))))))))))
  96. 0096congr
  97. 0097refl
  98. 0098trans ((u2) + ((u5) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u13) + ((u14) + (u15)))))))))))
  99. 0099congr
  100. 0100refl
  101. 0101apply four_square_add_swap_right_tail
  102. 0102apply four_square_add_swap_right_tail
  103. 0103apply four_square_add_swap_right_tail
  104. 0104congr
  105. 0105refl
  106. 0106congr
  107. 0107refl
  108. 0108trans ((u13) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15))))))))))
  109. 0109trans ((u2) + ((u13) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15))))))))))
  110. 0110congr
  111. 0111refl
  112. 0112trans ((u3) + ((u13) + ((u6) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15)))))))))
  113. 0113congr
  114. 0114refl
  115. 0115trans ((u6) + ((u13) + ((u7) + ((u9) + ((u10) + ((u11) + ((u14) + (u15))))))))
  116. 0116congr
  117. 0117refl
  118. 0118trans ((u7) + ((u13) + ((u9) + ((u10) + ((u11) + ((u14) + (u15)))))))
  119. 0119congr
  120. 0120refl
  121. 0121trans ((u9) + ((u13) + ((u10) + ((u11) + ((u14) + (u15))))))
  122. 0122congr
  123. 0123refl
  124. 0124trans ((u10) + ((u13) + ((u11) + ((u14) + (u15)))))
  125. 0125congr
  126. 0126refl
  127. 0127apply four_square_add_swap_right_tail
  128. 0128apply four_square_add_swap_right_tail
  129. 0129apply four_square_add_swap_right_tail
  130. 0130apply four_square_add_swap_right_tail
  131. 0131apply four_square_add_swap_right_tail
  132. 0132apply four_square_add_swap_right_tail
  133. 0133apply four_square_add_swap_right_tail
  134. 0134congr
  135. 0135refl
  136. 0136trans ((u11) + ((u2) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u14) + (u15)))))))))
  137. 0137trans ((u2) + ((u11) + ((u3) + ((u6) + ((u7) + ((u9) + ((u10) + ((u14) + (u15)))))))))
  138. 0138congr
  139. 0139refl
  140. 0140trans ((u3) + ((u11) + ((u6) + ((u7) + ((u9) + ((u10) + ((u14) + (u15))))))))
  141. 0141congr
  142. 0142refl
  143. 0143trans ((u6) + ((u11) + ((u7) + ((u9) + ((u10) + ((u14) + (u15)))))))
  144. 0144congr
  145. 0145refl
  146. 0146trans ((u7) + ((u11) + ((u9) + ((u10) + ((u14) + (u15))))))
  147. 0147congr
  148. 0148refl
  149. 0149trans ((u9) + ((u11) + ((u10) + ((u14) + (u15)))))
  150. 0150congr
  151. 0151refl
  152. 0152apply four_square_add_swap_right_tail
  153. 0153apply four_square_add_swap_right_tail
  154. 0154apply four_square_add_swap_right_tail
  155. 0155apply four_square_add_swap_right_tail
  156. 0156apply four_square_add_swap_right_tail
  157. 0157apply four_square_add_swap_right_tail
  158. 0158congr
  159. 0159refl
  160. 0160trans ((u9) + ((u2) + ((u3) + ((u6) + ((u7) + ((u10) + ((u14) + (u15))))))))
  161. 0161trans ((u2) + ((u9) + ((u3) + ((u6) + ((u7) + ((u10) + ((u14) + (u15))))))))
  162. 0162congr
  163. 0163refl
  164. 0164trans ((u3) + ((u9) + ((u6) + ((u7) + ((u10) + ((u14) + (u15)))))))
  165. 0165congr
  166. 0166refl
  167. 0167trans ((u6) + ((u9) + ((u7) + ((u10) + ((u14) + (u15))))))
  168. 0168congr
  169. 0169refl
  170. 0170apply four_square_add_swap_right_tail
  171. 0171apply four_square_add_swap_right_tail
  172. 0172apply four_square_add_swap_right_tail
  173. 0173apply four_square_add_swap_right_tail
  174. 0174congr
  175. 0175refl
  176. 0176trans ((u15) + ((u2) + ((u3) + ((u6) + ((u7) + ((u10) + (u14)))))))
  177. 0177trans ((u2) + ((u15) + ((u3) + ((u6) + ((u7) + ((u10) + (u14)))))))
  178. 0178congr
  179. 0179refl
  180. 0180trans ((u3) + ((u15) + ((u6) + ((u7) + ((u10) + (u14))))))
  181. 0181congr
  182. 0182refl
  183. 0183trans ((u6) + ((u15) + ((u7) + ((u10) + (u14)))))
  184. 0184congr
  185. 0185refl
  186. 0186trans ((u7) + ((u15) + ((u10) + (u14))))
  187. 0187congr
  188. 0188refl
  189. 0189trans ((u10) + ((u15) + (u14)))
  190. 0190congr
  191. 0191refl
  192. 0192apply add_comm
  193. 0193apply four_square_add_swap_right_tail
  194. 0194apply four_square_add_swap_right_tail
  195. 0195apply four_square_add_swap_right_tail
  196. 0196apply four_square_add_swap_right_tail
  197. 0197apply four_square_add_swap_right_tail
  198. 0198congr
  199. 0199refl
  200. 0200congr
  201. 0201refl
  202. 0202trans ((u6) + ((u3) + ((u7) + ((u10) + (u14)))))
  203. 0203apply four_square_add_swap_right_tail
  204. 0204congr
  205. 0205refl
  206. 0206trans ((u14) + ((u3) + ((u7) + (u10))))
  207. 0207trans ((u3) + ((u14) + ((u7) + (u10))))
  208. 0208congr
  209. 0209refl
  210. 0210trans ((u7) + ((u14) + (u10)))
  211. 0211congr
  212. 0212refl
  213. 0213apply add_comm
  214. 0214apply four_square_add_swap_right_tail
  215. 0215apply four_square_add_swap_right_tail
  216. 0216congr
  217. 0217refl
  218. 0218trans ((u10) + ((u3) + (u7)))
  219. 0219trans ((u3) + ((u10) + (u7)))
  220. 0220congr
  221. 0221refl
  222. 0222apply add_comm
  223. 0223apply four_square_add_swap_right_tail
  224. 0224congr
  225. 0225refl
  226. 0226trans ((u7) + (u3))
  227. 0227apply add_comm
  228. 0228congr
  229. 0229refl
  230. 0230refl
  231. 0231symm
  232. 0232simp [add_assoc]