Commit 948b65e0 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Untrack generated file drinker.dk

parent e2df7571
#NAME drinker.
BAR : fol.type.
JOE : fol.function.
[] fol.fun_arity (JOE) --> fol.nil_type.
[] fol.fun_codomain (JOE) --> BAR.
def Joe : fol.term BAR := fol.apply_fun JOE fol.nil_term.
DRINK : fol.predicate.
[] fol.pred_arity (DRINK) --> fol.read_types (nat.S nat.O) BAR.
def drink :
x:(fol.term BAR) -> fol.prop
:=
x:(fol.term BAR) =>
fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term).
def drinker_statement :
fol.prop
:=
fol.ex BAR
(x:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term))
(fol.all BAR
(x0:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term)))).
def ndrink :=
x:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term))
fol.false.
def drinker_paradox :
c:fol.prop ->
(a:(fol.term BAR) ->
((fol.proof
(fol.apply_pred DRINK (fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
a0:(fol.term BAR) ->
fol.proof
(fol.apply_pred DRINK (fol.cons_term BAR a0 fol.nil_type fol.nil_term))) ->
fol.proof c) ->
fol.proof c
:=
classical.excluded_middle
(fol.all BAR
(x:(fol.term BAR) =>
fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term)))
(fol.ex BAR
(x:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x fol.nil_type fol.nil_term))
(fol.all BAR
(x0:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term)))))
(x:
(a:(fol.term BAR) ->
fol.proof
(fol.apply_pred DRINK (fol.cons_term BAR a fol.nil_type fol.nil_term))) =>
fol.ex_intro BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
(fol.all BAR
(x1:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))))
(fol.apply_fun JOE fol.nil_term)
(x0:
(fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR (fol.apply_fun JOE fol.nil_term)
fol.nil_type fol.nil_term))) =>
x))
(x:
((a:(fol.term BAR) ->
fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
c:fol.prop -> fol.proof c) =>
fol.ex_elim BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term)) fol.false)
(fol.ex BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
(fol.all BAR
(x1:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term)))))
(classical.excluded_middle
(fol.ex BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
fol.false))
(fol.ex BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
fol.false))
(x0:
(c:fol.prop ->
(a:(fol.term BAR) ->
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
c0:fol.prop -> fol.proof c0) ->
fol.proof c) ->
fol.proof c) =>
x0)
(x0:
((c:fol.prop ->
(a:(fol.term BAR) ->
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
c0:fol.prop -> fol.proof c0) ->
fol.proof c) ->
fol.proof c) ->
c:fol.prop -> fol.proof c) =>
fol.false_elim
(fol.ex BAR
(x1:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
fol.false))
(x
(x1:(fol.term BAR) =>
classical.excluded_middle
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
(x2:
(fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))) =>
x2)
(x2:
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))) ->
c:fol.prop -> fol.proof c) =>
fol.false_elim
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
(x0
(fol.ex_intro BAR
(x3 =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x3 fol.nil_type
fol.nil_term)) fol.false) x1 x2)))))))
(x0:(fol.term BAR) =>
x1:
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))) ->
c:fol.prop -> fol.proof c) =>
fol.ex_intro BAR
(x2:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x2 fol.nil_type fol.nil_term))
(fol.all BAR
(x3:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x3 fol.nil_type fol.nil_term)))) x0
(x2:
(fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))) =>
fol.false_elim
(fol.all BAR
(x3:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x3 fol.nil_type fol.nil_term))) (
x1 x2)))).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment