FS002L

four_square_euler_add_permute_twelve

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The twelve paired Hamilton mixed blocks are placed in their four signed-coordinate correction groups.

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.

Exact expanded first-order arithmetic statement

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

Constructive proof overview

Generated structural guide

The twelve paired Hamilton mixed blocks are placed in their four signed-coordinate correction groups.

The unchanged tactic script uses 3 declared prerequisites and contains 178 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized FS0006 four_square_add_swap_right_tail

Direct dependents

FS002W four_square_euler_mixed_decomposition

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

178 script commands · 30 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.

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–12

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

  1. L11
    intro u10
  2. L12
    intro u11
03Calculate and transport equalitiesL13–22

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

  1. L13
    trans ((u0) + ((u1) + ((u2) + ((u3) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))))
  2. L14
    simp [add_assoc]
  3. L15
    trans ((u3) + ((u6) + ((u10) + ((u7) + ((u11) + ((u2) + ((u9) + ((u5) + ((u1) + ((u4) + ((u0) + (u8))))))))))))
  4. L16
    trans ((u3) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))))
  5. L17
    trans ((u0) + ((u3) + ((u1) + ((u2) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))))
  6. L18
    congr
  7. L19
    refl
  8. L20
    trans ((u1) + ((u3) + ((u2) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))))
  9. L21
    congr
  10. L22
    refl
04Use earlier factsL23–25

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

  1. L23
    apply four_square_add_swap_right_tail
  2. L24
    apply four_square_add_swap_right_tail
  3. L25
    apply four_square_add_swap_right_tail
05Calculate and transport equalitiesL26–35

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

  1. L26
    congr
  2. L27
    refl
  3. L28
    trans ((u6) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))))
  4. L29
    trans ((u0) + ((u6) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))))
  5. L30
    congr
  6. L31
    refl
  7. L32
    trans ((u1) + ((u6) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))
  8. L33
    congr
  9. L34
    refl
  10. L35
    trans ((u2) + ((u6) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))
06Calculate and transport equalitiesL36–40

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

  1. L36
    congr
  2. L37
    refl
  3. L38
    trans ((u4) + ((u6) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))
  4. L39
    congr
  5. L40
    refl
07Use earlier factsL41–45

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

  1. L41
    apply four_square_add_swap_right_tail
  2. L42
    apply four_square_add_swap_right_tail
  3. L43
    apply four_square_add_swap_right_tail
  4. L44
    apply four_square_add_swap_right_tail
  5. L45
    apply four_square_add_swap_right_tail
08Calculate and transport equalitiesL46–55

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

  1. L46
    congr
  2. L47
    refl
  3. L48
    trans ((u10) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11))))))))))
  4. L49
    trans ((u0) + ((u10) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11))))))))))
  5. L50
    congr
  6. L51
    refl
  7. L52
    trans ((u1) + ((u10) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11)))))))))
  8. L53
    congr
  9. L54
    refl
  10. L55
    trans ((u2) + ((u10) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11))))))))
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 ((u4) + ((u10) + ((u5) + ((u7) + ((u8) + ((u9) + (u11)))))))
  4. L59
    congr
  5. L60
    refl
  6. L61
    trans ((u5) + ((u10) + ((u7) + ((u8) + ((u9) + (u11))))))
  7. L62
    congr
  8. L63
    refl
  9. L64
    trans ((u7) + ((u10) + ((u8) + ((u9) + (u11)))))
  10. L65
    congr
10Calculate and transport equalitiesL66–69

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

  1. L66
    refl
  2. L67
    trans ((u8) + ((u10) + ((u9) + (u11))))
  3. L68
    congr
  4. L69
    refl
11Use earlier factsL70–77

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

  1. L70
    apply four_square_add_swap_right_tail
  2. L71
    apply four_square_add_swap_right_tail
  3. L72
    apply four_square_add_swap_right_tail
  4. L73
    apply four_square_add_swap_right_tail
  5. L74
    apply four_square_add_swap_right_tail
  6. L75
    apply four_square_add_swap_right_tail
  7. L76
    apply four_square_add_swap_right_tail
  8. L77
    apply four_square_add_swap_right_tail
12Calculate and transport equalitiesL78–87

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

  1. L78
    congr
  2. L79
    refl
  3. L80
    trans ((u7) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + ((u9) + (u11)))))))))
  4. L81
    trans ((u0) + ((u7) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + ((u9) + (u11)))))))))
  5. L82
    congr
  6. L83
    refl
  7. L84
    trans ((u1) + ((u7) + ((u2) + ((u4) + ((u5) + ((u8) + ((u9) + (u11))))))))
  8. L85
    congr
  9. L86
    refl
  10. L87
    trans ((u2) + ((u7) + ((u4) + ((u5) + ((u8) + ((u9) + (u11)))))))
13Calculate and transport equalitiesL88–92

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

  1. L88
    congr
  2. L89
    refl
  3. L90
    trans ((u4) + ((u7) + ((u5) + ((u8) + ((u9) + (u11))))))
  4. L91
    congr
  5. L92
    refl
14Use earlier factsL93–97

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

  1. L93
    apply four_square_add_swap_right_tail
  2. L94
    apply four_square_add_swap_right_tail
  3. L95
    apply four_square_add_swap_right_tail
  4. L96
    apply four_square_add_swap_right_tail
  5. L97
    apply four_square_add_swap_right_tail
15Calculate and transport equalitiesL98–107

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

  1. L98
    congr
  2. L99
    refl
  3. L100
    trans ((u11) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + (u9))))))))
  4. L101
    trans ((u0) + ((u11) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + (u9))))))))
  5. L102
    congr
  6. L103
    refl
  7. L104
    trans ((u1) + ((u11) + ((u2) + ((u4) + ((u5) + ((u8) + (u9)))))))
  8. L105
    congr
  9. L106
    refl
  10. L107
    trans ((u2) + ((u11) + ((u4) + ((u5) + ((u8) + (u9))))))
16Calculate and transport equalitiesL108–117

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

  1. L108
    congr
  2. L109
    refl
  3. L110
    trans ((u4) + ((u11) + ((u5) + ((u8) + (u9)))))
  4. L111
    congr
  5. L112
    refl
  6. L113
    trans ((u5) + ((u11) + ((u8) + (u9))))
  7. L114
    congr
  8. L115
    refl
  9. L116
    trans ((u8) + ((u11) + (u9)))
  10. L117
    congr
17Calculate and transport equalitiesL118–118

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

  1. L118
    refl
18Use earlier factsL119–125

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

  1. L119
    apply add_comm
  2. L120
    apply four_square_add_swap_right_tail
  3. L121
    apply four_square_add_swap_right_tail
  4. L122
    apply four_square_add_swap_right_tail
  5. L123
    apply four_square_add_swap_right_tail
  6. L124
    apply four_square_add_swap_right_tail
  7. L125
    apply four_square_add_swap_right_tail
19Calculate and transport equalitiesL126–131

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

  1. L126
    congr
  2. L127
    refl
  3. L128
    trans ((u2) + ((u0) + ((u1) + ((u4) + ((u5) + ((u8) + (u9)))))))
  4. L129
    trans ((u0) + ((u2) + ((u1) + ((u4) + ((u5) + ((u8) + (u9)))))))
  5. L130
    congr
  6. L131
    refl
20Use earlier factsL132–133

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

  1. L132
    apply four_square_add_swap_right_tail
  2. L133
    apply four_square_add_swap_right_tail
21Calculate 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 ((u9) + ((u0) + ((u1) + ((u4) + ((u5) + (u8))))))
  4. L137
    trans ((u0) + ((u9) + ((u1) + ((u4) + ((u5) + (u8))))))
  5. L138
    congr
  6. L139
    refl
  7. L140
    trans ((u1) + ((u9) + ((u4) + ((u5) + (u8)))))
  8. L141
    congr
  9. L142
    refl
  10. L143
    trans ((u4) + ((u9) + ((u5) + (u8))))
22Calculate and transport equalitiesL144–148

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 ((u5) + ((u9) + (u8)))
  4. L147
    congr
  5. L148
    refl
23Use earlier factsL149–153

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

  1. L149
    apply add_comm
  2. L150
    apply four_square_add_swap_right_tail
  3. L151
    apply four_square_add_swap_right_tail
  4. L152
    apply four_square_add_swap_right_tail
  5. L153
    apply four_square_add_swap_right_tail
24Calculate and transport equalitiesL154–162

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

  1. L154
    congr
  2. L155
    refl
  3. L156
    trans ((u5) + ((u0) + ((u1) + ((u4) + (u8)))))
  4. L157
    trans ((u0) + ((u5) + ((u1) + ((u4) + (u8)))))
  5. L158
    congr
  6. L159
    refl
  7. L160
    trans ((u1) + ((u5) + ((u4) + (u8))))
  8. L161
    congr
  9. L162
    refl
25Use earlier factsL163–165

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

  1. L163
    apply four_square_add_swap_right_tail
  2. L164
    apply four_square_add_swap_right_tail
  3. L165
    apply four_square_add_swap_right_tail
26Calculate and transport equalitiesL166–168

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

  1. L166
    congr
  2. L167
    refl
  3. L168
    trans ((u1) + ((u0) + ((u4) + (u8))))
27Use earlier factsL169–169

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

  1. L169
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL170–172

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

  1. L170
    congr
  2. L171
    refl
  3. L172
    trans ((u4) + ((u0) + (u8)))
29Use earlier factsL173–173

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

  1. L173
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL174–178

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
    refl
  4. L177
    symm
  5. L178
    simp [add_assoc]

Library-wide reading audit

Original exact command ledger · 178 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. 0013trans ((u0) + ((u1) + ((u2) + ((u3) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))))
  14. 0014simp [add_assoc]
  15. 0015trans ((u3) + ((u6) + ((u10) + ((u7) + ((u11) + ((u2) + ((u9) + ((u5) + ((u1) + ((u4) + ((u0) + (u8))))))))))))
  16. 0016trans ((u3) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))))
  17. 0017trans ((u0) + ((u3) + ((u1) + ((u2) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))))
  18. 0018congr
  19. 0019refl
  20. 0020trans ((u1) + ((u3) + ((u2) + ((u4) + ((u5) + ((u6) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))))
  21. 0021congr
  22. 0022refl
  23. 0023apply four_square_add_swap_right_tail
  24. 0024apply four_square_add_swap_right_tail
  25. 0025apply four_square_add_swap_right_tail
  26. 0026congr
  27. 0027refl
  28. 0028trans ((u6) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))))
  29. 0029trans ((u0) + ((u6) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))))
  30. 0030congr
  31. 0031refl
  32. 0032trans ((u1) + ((u6) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))))
  33. 0033congr
  34. 0034refl
  35. 0035trans ((u2) + ((u6) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11)))))))))
  36. 0036congr
  37. 0037refl
  38. 0038trans ((u4) + ((u6) + ((u5) + ((u7) + ((u8) + ((u9) + ((u10) + (u11))))))))
  39. 0039congr
  40. 0040refl
  41. 0041apply four_square_add_swap_right_tail
  42. 0042apply four_square_add_swap_right_tail
  43. 0043apply four_square_add_swap_right_tail
  44. 0044apply four_square_add_swap_right_tail
  45. 0045apply four_square_add_swap_right_tail
  46. 0046congr
  47. 0047refl
  48. 0048trans ((u10) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11))))))))))
  49. 0049trans ((u0) + ((u10) + ((u1) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11))))))))))
  50. 0050congr
  51. 0051refl
  52. 0052trans ((u1) + ((u10) + ((u2) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11)))))))))
  53. 0053congr
  54. 0054refl
  55. 0055trans ((u2) + ((u10) + ((u4) + ((u5) + ((u7) + ((u8) + ((u9) + (u11))))))))
  56. 0056congr
  57. 0057refl
  58. 0058trans ((u4) + ((u10) + ((u5) + ((u7) + ((u8) + ((u9) + (u11)))))))
  59. 0059congr
  60. 0060refl
  61. 0061trans ((u5) + ((u10) + ((u7) + ((u8) + ((u9) + (u11))))))
  62. 0062congr
  63. 0063refl
  64. 0064trans ((u7) + ((u10) + ((u8) + ((u9) + (u11)))))
  65. 0065congr
  66. 0066refl
  67. 0067trans ((u8) + ((u10) + ((u9) + (u11))))
  68. 0068congr
  69. 0069refl
  70. 0070apply four_square_add_swap_right_tail
  71. 0071apply four_square_add_swap_right_tail
  72. 0072apply four_square_add_swap_right_tail
  73. 0073apply four_square_add_swap_right_tail
  74. 0074apply four_square_add_swap_right_tail
  75. 0075apply four_square_add_swap_right_tail
  76. 0076apply four_square_add_swap_right_tail
  77. 0077apply four_square_add_swap_right_tail
  78. 0078congr
  79. 0079refl
  80. 0080trans ((u7) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + ((u9) + (u11)))))))))
  81. 0081trans ((u0) + ((u7) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + ((u9) + (u11)))))))))
  82. 0082congr
  83. 0083refl
  84. 0084trans ((u1) + ((u7) + ((u2) + ((u4) + ((u5) + ((u8) + ((u9) + (u11))))))))
  85. 0085congr
  86. 0086refl
  87. 0087trans ((u2) + ((u7) + ((u4) + ((u5) + ((u8) + ((u9) + (u11)))))))
  88. 0088congr
  89. 0089refl
  90. 0090trans ((u4) + ((u7) + ((u5) + ((u8) + ((u9) + (u11))))))
  91. 0091congr
  92. 0092refl
  93. 0093apply four_square_add_swap_right_tail
  94. 0094apply four_square_add_swap_right_tail
  95. 0095apply four_square_add_swap_right_tail
  96. 0096apply four_square_add_swap_right_tail
  97. 0097apply four_square_add_swap_right_tail
  98. 0098congr
  99. 0099refl
  100. 0100trans ((u11) + ((u0) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + (u9))))))))
  101. 0101trans ((u0) + ((u11) + ((u1) + ((u2) + ((u4) + ((u5) + ((u8) + (u9))))))))
  102. 0102congr
  103. 0103refl
  104. 0104trans ((u1) + ((u11) + ((u2) + ((u4) + ((u5) + ((u8) + (u9)))))))
  105. 0105congr
  106. 0106refl
  107. 0107trans ((u2) + ((u11) + ((u4) + ((u5) + ((u8) + (u9))))))
  108. 0108congr
  109. 0109refl
  110. 0110trans ((u4) + ((u11) + ((u5) + ((u8) + (u9)))))
  111. 0111congr
  112. 0112refl
  113. 0113trans ((u5) + ((u11) + ((u8) + (u9))))
  114. 0114congr
  115. 0115refl
  116. 0116trans ((u8) + ((u11) + (u9)))
  117. 0117congr
  118. 0118refl
  119. 0119apply add_comm
  120. 0120apply four_square_add_swap_right_tail
  121. 0121apply four_square_add_swap_right_tail
  122. 0122apply four_square_add_swap_right_tail
  123. 0123apply four_square_add_swap_right_tail
  124. 0124apply four_square_add_swap_right_tail
  125. 0125apply four_square_add_swap_right_tail
  126. 0126congr
  127. 0127refl
  128. 0128trans ((u2) + ((u0) + ((u1) + ((u4) + ((u5) + ((u8) + (u9)))))))
  129. 0129trans ((u0) + ((u2) + ((u1) + ((u4) + ((u5) + ((u8) + (u9)))))))
  130. 0130congr
  131. 0131refl
  132. 0132apply four_square_add_swap_right_tail
  133. 0133apply four_square_add_swap_right_tail
  134. 0134congr
  135. 0135refl
  136. 0136trans ((u9) + ((u0) + ((u1) + ((u4) + ((u5) + (u8))))))
  137. 0137trans ((u0) + ((u9) + ((u1) + ((u4) + ((u5) + (u8))))))
  138. 0138congr
  139. 0139refl
  140. 0140trans ((u1) + ((u9) + ((u4) + ((u5) + (u8)))))
  141. 0141congr
  142. 0142refl
  143. 0143trans ((u4) + ((u9) + ((u5) + (u8))))
  144. 0144congr
  145. 0145refl
  146. 0146trans ((u5) + ((u9) + (u8)))
  147. 0147congr
  148. 0148refl
  149. 0149apply add_comm
  150. 0150apply four_square_add_swap_right_tail
  151. 0151apply four_square_add_swap_right_tail
  152. 0152apply four_square_add_swap_right_tail
  153. 0153apply four_square_add_swap_right_tail
  154. 0154congr
  155. 0155refl
  156. 0156trans ((u5) + ((u0) + ((u1) + ((u4) + (u8)))))
  157. 0157trans ((u0) + ((u5) + ((u1) + ((u4) + (u8)))))
  158. 0158congr
  159. 0159refl
  160. 0160trans ((u1) + ((u5) + ((u4) + (u8))))
  161. 0161congr
  162. 0162refl
  163. 0163apply four_square_add_swap_right_tail
  164. 0164apply four_square_add_swap_right_tail
  165. 0165apply four_square_add_swap_right_tail
  166. 0166congr
  167. 0167refl
  168. 0168trans ((u1) + ((u0) + ((u4) + (u8))))
  169. 0169apply four_square_add_swap_right_tail
  170. 0170congr
  171. 0171refl
  172. 0172trans ((u4) + ((u0) + (u8)))
  173. 0173apply four_square_add_swap_right_tail
  174. 0174congr
  175. 0175refl
  176. 0176refl
  177. 0177symm
  178. 0178simp [add_assoc]