ax10ex

Theorem.

Arguments:

(sv), (sv), (pr),

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	ax10b	1	(()())
	aln.ex	2	()
	aln.ex	3	()
1, 2, 3	>2bitrg	4	(()())
4	bi.bldnegd	5	(()())
	bneg>	6	()
	bneg>	7	()
5, 6, 7	<2bitrg	8	(()())