theorem
proved
term proof
rungValue_zero
show as:
view Lean formalization →
formal statement (Lean)
32@[simp] theorem rungValue_zero : rungValue 0 = 1 := by
proof body
Term-mode proof.
33 unfold rungValue
34 norm_num
35
36/-- One finite 8-Balanced J-Subset Sum instance. -/