-- Maclain Hunter: Debunking Maxwell’s Demon
-- Exact authored source SHA-256: 0c9519b04feccba16361930ca28f487527e873969d45c94bed04b8bfba81f1b5
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

theorem inference_1 (v0 v1 v2 : Bool) :
    ((!((v1 && ((!v1) || v2)) && ((!v2) || v0))) || ((v1 && v2) && v0)) = true := by
  cases v0 <;> cases v1 <;> cases v2 <;> decide
#print axioms inference_1

theorem inference_2 (v0 v1 v2 : Bool) :
    ((!(((!v1) && ((!(!v1)) || (!v2))) && ((!(!v2)) || (!v0)))) || (((!v1) && (!v2)) && (!v0))) = true := by
  cases v0 <;> cases v1 <;> cases v2 <;> decide
#print axioms inference_2

end HunterAuthored