>(1R)o(1R)^(2L)v(2L)-=AE    /Symbols allowed
pred, func, const, sent   /Parameter categories allowed.
mp    /First rule is mp (modus ponens).
P     /It says that from P
P>Q   /and P->Q
:Q    /you can infer Q.
adj   /adjunction
P
Q
:P^Q
si    /self-implication
:gen(P>P)
suff   /suffixing
:gen((P>Q)>((Q>R)>(P>R)))
id     /implication distribution
:gen((P>(Q>R))>((P>Q)>(P>R)))
perm   /permutation
:gen((P>(Q>R))>(Q>(P>R)))
ce1    /conjunction elimination I
:gen((P^Q)>P)
ce2   /conjunction elimination II
:gen((P^Q)>Q)
ci     /conjunction introduction
:gen(((P>Q)^(P>R))>(P>(Q^R)))
de     /disjunction elimination
:gen(((P>R)^(Q>R))>((PvQ)>R))
di1    /disjunction introduction I
:gen(P>(PvQ))
di2   /disjunction introduction II
:gen(Q>(PvQ))
dist   /distribution
:gen((P^(QvR))>((P^Q)v(P^R)))
fi     /fusion introduction
:gen(P>(Q>(PoQ)))
res2  /residuation II
:gen((P>(Q>R))>((PoQ)>R))
red    /reductio
:gen(P>-P)>-P
ic     /intuitionistic contraposition
:gen((P>-Q)>(Q>-P))
dn     /double negation
:gen(--P>P)
ui     /universal instantiation
:gen(AxP>P[x|a])
ud     /universal quantifier distribution
:gen(Ax(P>Q)>(AxP>AxQ))
vug    /vacuous universal generalization
:gen(P[x*]>AxP)
uc     /universal confinement
:gen(Ax(P[x*]vQ)>(PvAxQ))
eg     /existential generalization
:gen(P[x|a]>ExP)
ed     /existential quantifier distribution
:gen(Ax(P>Q)>(ExP>ExQ))
vei    /vacuous existential instantiation
:gen(ExP>P[x*])
ec     /existential confinement
:gen((P[x*]^ExQ)>Ex(P^Q))
ref    /reflexive
:gen(x=x)
sub    /substitution
:gen(x=y>P>P[x?y])