%read "prop.elf".
%read "../syntax/derived.elf".
%sig FalsityPFExt = {
%include FalsityPF %open.
falseE' : ded false -> ded A = [p] falseE p A.
}.
%sig NEGPFExt = {
%include NEGPF %open.
notE' : ded A -> ded not A -> ded B = [p][q] notE q p B.
nn : o -> o = [x] not not x.
notnotI : ded A -> ded nn A = [p] notI ([q][_] notE' p q).
int_notnotE : ded nn not A -> ded not A
= [p] notI [q][_] notE' (notnotI q) p.
}.
%sig IMPPFExt = {
%include IMPPF %open.
imp2I : (ded A -> ded B -> ded C) -> ded A imp (B imp C) = [f] impI [p] impI [q] f p q.
imp2E : ded A imp (B imp C) -> ded A -> ded B -> ded C = [p][q][r] impE (impE p q) r.
}.
%sig CONJPFExt = {
%include CONJPF %open.
and3I : ded A -> ded B -> ded C -> ded A and B and C
= [p][q][r] andI (andI p q) r.
and3El : ded A and B and C -> ded A = [p] andEl (andEl p).
and3Em : ded A and B and C -> ded B = [p] andEr (andEl p).
and3Er : ded A and B and C -> ded C = andEr.
and_comm : ded A and B -> ded B and A = [p] andI (andEr p) (andEl p).
and_assl : ded (A and B) and C -> ded A and (B and C) = [p] andI (and3El p) (andI (and3Em p) (and3Er p)).
and_assr : ded A and (B and C) -> ded (A and B) and C = [p] and3I (andEl p) (andEl (andEr p)) (andEr (andEr p)).
and_idem : ded A -> ded A and A = [p] andI p p.
}.
%sig DISJPFExt = {
%include DISJPF %open.
or3Il : ded A -> ded A or B or C = [p] orIl (orIl p).
or3Im : ded B -> ded A or B or C = [p] orIl (orIr p).
or3Ir : ded C -> ded A or B or C = orIr.
or3E : ded A or B or C -> (ded A -> ded D) -> (ded B -> ded D) -> (ded C -> ded D) -> ded D
= [p][f][g][h] orE p ([q] orE q f g) h.
or_comm : ded A or B -> ded B or A = [p] orE p orIr orIl.
or_assl : ded (A or B) or C -> ded A or (B or C) = [p] or3E p orIl ([r] orIr (orIl r)) ([r] orIr (orIr r)).
or_assr : ded A or (B or C) -> ded (A or B) or C = [p] orE p or3Il ([q] orE q or3Im or3Ir).
or_idem : ded A or A -> ded A = [p] orE p ([q]q) ([q]q).
}.
%sig EquivPF = {
%include Equiv %open.
%include CONJPF %open.
%include IMPPF %open.
equivI : (ded A -> ded B) -> (ded B -> ded A) -> ded A equiv B = [f][g] andI (impI f) (impI g).
equivEl : ded A equiv B -> ded A -> ded B = [p] [a] impE (andEl p) a.
equivEr : ded A equiv B -> ded B -> ded A = [p] [b] impE (andEr p) b.
equiv_refl : ded A equiv A = equivI ([a] a) ([a] a).
equiv_sym : ded A equiv B -> ded B equiv A
= [p] equivI ([b] equivEr p b) ([a] equivEl p a).
equiv_trans : ded A equiv B -> ded B equiv C -> ded A equiv C
= [p][q] equivI ([a] equivEl q (equivEl p a)) ([c] equivEr p (equivEr q c)).
}.
%sig PLPFExt = {
%include CPLPF %open.
%include FalsityPFExt %open.
%include NEGPFExt %open.
%include IMPPFExt %open.
%include CONJPFExt %open.
%include DISJPFExt %open.
%include EquivPF %open.
nnotE : ded not (not A) -> ded A = [p] orE tnd ([q:ded A] q) ([q: ded not A] notE' q p).
indir : (ded not A -> {B} ded B) -> ded A = [f] nnotE (notI ([p: ded not A] f p)).
norEl : ded not (A or B) -> ded not A = [p] notI [q] notE p (orIl q).
norEr : ded not (A or B) -> ded not B = [p] notI [q] notE p (orIr q).
nimpEl : ded not (A imp B) -> ded A = [p] indir [q] notE p (impI ([r] notE' r q)).
nimpEr : ded not (A imp B) -> ded not B = [p] notI [q] notE p (impI [r] q).
}.