Skip to content

Instantly share code, notes, and snippets.

@philzook58

philzook58/gist:ba7d8a26db2fd5d9f92f7b54ab314c0e

Created December 20, 2024 15:51
Show Gist options
  • Save philzook58/ba7d8a26db2fd5d9f92f7b54ab314c0e to your computer and use it in GitHub Desktop.
Save philzook58/ba7d8a26db2fd5d9f92f7b54ab314c0e to your computer and use it in GitHub Desktop.
Download ZIP
knuckeldragger add comm
Raw
gistfile1.txt
l = kd.Lemma(smt.ForAll([x,y], add(x, y) == add(y, x)))
x1,y1 = l.intros()
l.induct(x1)
l.auto(by=[add.defn, add_Z_r])
z1 = l.fixes()
l.auto(by=[add.defn, add_s_r])
add_comm = l.qed()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment