PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
zero
rank
all
vars
1
1
1
1.
L:
Sequent List
2.
eqS:
{Sequent=
}
3.
eqF:
{Formula=
}
4.
s
L.(
(s) = 0)
5.
hyp:
Formula List
6.
concl:
Formula List
7.
< hyp,concl > (
eqS) L
8.
z:
Formula
9.
z(
eqF) hyp
10.
( < hyp,concl > ) = 0
v:Var. z =
v
By:
AbReduce -1
Generated subgoal:
1
10.
(hyp)+
(concl) = 0
v:Var. z =
v
About:
(hyp)+(concl) = 0
v:Var. z = 
v
}}
s
L.((s) = 0)eqS) LeqF) hyp( < hyp,concl > ) = 0 v:Var. z = v(hyp)+(concl) = 0 v:Var. z = v
