begin	comment Bewijstester voor logische uitspraken. R 1082;
	integer a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z,
		last, ow, hw, tw, opw;
	integer array OP, ARG1, ARG2[1 : 1000], CODE, NOP[1 : 20], TR[3 : 20], T[1 : 500], H, TBV, OPW[1 : 20], F[1 : 100];
	Boolean array M, N[-26 : -1];

	procedure error (fout, diagnose, indicatie); value fout, indicatie; Boolean fout; string diagnose; integer indicatie;
	if fout then
	begin	PUNLCR; PUTEXT ("fout: "); PUTEXT (diagnose);
		PUSPACE (1); PUNCH (indicatie); dump; EXIT
	end;

	procedure dump;
	begin	integer k;
		PRINTTEXT ("op + arg1 + arg2");
		for k:= 1 step 1 until ow do
		begin NLCR; PRINT (k); PRINT (OP[k]); PRINT (ARG1[k]); PRINT (ARG2[k]) end;
		NLCR; PRINTTEXT ("code + nop + tr");
		for k:= 1 step 1 until opw do
		begin NLCR; PRINT (k); PRINT (CODE[k]); PRINT (NOP[k]); if k >= 3 then PRINT (TR[k]) end;
		NLCR; PRINTTEXT ("t");
		for k:= 1 step 1 until tw do
		begin NLCR; PRINT (k); PRINT (T[k]) end;
		NLCR; PRINTTEXT ("h + tbv + opw");
		for k:= 1 step 1 until hw do
		begin NLCR; PRINT (k); PRINT (H[k]); PRINT (TBV[k]); if TBV[k] < 0 then PRINT (OPW[k]) end;
		NLCR; PRINTTEXT ("m");
		for k:= -1 step -1 until -26 do
		begin NLCR; PRINT (k); if M[k] then PRINTTEXT ("true") else PRINTTEXT ("false") end
	end;

	integer procedure form2 (op, arg1, arg2); value op, arg1, arg2; integer op, arg1, arg2;
	begin	integer k;
		for k:= ow step -1 until 1 do
		if op != OP[k] then else if arg1 != ARG1[k] then else if arg2 = ARG2[k] then
		begin form2:= k; go to exit end;
		form2:= ow:= ow + 1; OP[ow]:= op; ARG1[ow]:= arg1; ARG2[ow]:= arg2;
	exit:
	end;

	integer procedure form1 (op, arg); integer op, arg;
	form1:= form2 (op, arg, 0);

	integer procedure opwijz (op); value op; integer op;
	begin	integer k;
		for k:= opw step -1 until 1 do if CODE[k] = op then
		begin opwijz:= k; go to exit end;
		opwijz:= 0;
	exit:
	end;

	procedure test (x); value x; integer x;
	if x < 0 then error (! M[x], "onbekende variabele", x) else
	begin	integer op, opw, a1, a2;
		error (x < 1 | x > ow, "formule is onzin", x);
		op:= OP[x]; a1:= ARG1[x]; a2:= ARG2[x]; opw:= opwijz (op);
		error (opw = 0, "onbekende operator", op);
		error (a2 = 0 == NOP[opw] = 2, "onjuist aantal operanden", op);
		if op = al then
		begin onbek (a1); test (a2); M[a1]:= false end else
		begin test (a1); if a2 != 0 then test (a2) end
	end;

	procedure Definieer (op, code, L, R); value code; integer op, code, L, R;
	begin	integer a1, a2, LL, RR;
		error (opwijz (code) != 0, "te definieren operator reeds bekend", code);
		op:= code; LL:= L;
		error (OP[LL] != code, "fout in definitie", code);
		a1:= ARG1[LL]; a2:= ARG2[LL]; onbek (a1); if a2 != 0 then onbek (a2);
		RR:= R; test (RR); M[a1]:= false; if a2 != 0 then M[a2]:= false;
		opw:= opw + 1; NOP[opw]:= if a2 = 0 then 1 else 2; CODE[opw]:= code;
		TR[opw]:= if a2 = 0 then A (a1, RR) else A (a1, A (a2, RR));
		NL; uit (LL); PUTEXT (" is gedefinieerd als "); uit (RR); PUNLCR
	end;

	procedure NL;
	begin	integer k;
		PUNLCR; for k:= 1 step 1 until hw do PUSYM (118)
	end;
	procedure NL1;
	begin	integer k;
		PUNLCR; for k:= 2 step 1 until hw do PUSYM (118)
	end;

	procedure onbek (x); value x; integer x;
	begin error (M[x], "variabele reeds bekend", x); M[x]:= true end;

	integer procedure store (a); value a; integer a;
	begin tw:= tw + 1; store:= T[tw]:= uit (a) end;

	integer procedure uit (a); value a; integer a;
	begin	if a < 0 then PUSYM (9 - a) else if ARG2[a] = 0 then
		begin opuit (OP[a]); PUSPACE (1); uit (ARG1[a]) end else
		if OP[a] = al then
		begin opuit (al); PUSPACE (1); uit (ARG1[a]); PUTEXT (": "); uit (ARG2[a]) end else
		begin PUTEXT ("("); uit (ARG1[a]); PUSPACE (1); opuit (OP[a]); PUSPACE (1); uit (ARG2[a]); PUTEXT (")") end;
		uit:= last:= a
	end;

	procedure opuit (z); value z; integer z;
	begin	integer q;
		for q:= z % 1000 while z != 0 do
		begin PUSYM (z - 1000 * q); z:= q end
	end;

	integer procedure al; al:= 037126; comment A;
	integer procedure impl; impl:= 074070; comment =>;

	integer procedure A (x, y); integer x, y;
	A:= form2 (al, x, y);

	integer procedure Impl (x, y); integer x, y;
	Impl:= form2 (impl, x, y);

	integer procedure Concl (a, c); value a, c; integer a, c;
	begin	integer b;
		testproven(c, "a => b in Concl", true); testproven (a, "a in Concl", false);
		error (OP[c] != impl | ARG1[c] != a, "Concl niet van toepassing", c);
		b:= ARG2[c]; NL; PUTEXT ("Dus "); Concl:= store (b)
	end;

	procedure testproven (a, s, cr); value a, cr; integer a; string s; Boolean cr;
	begin	integer k;
		if a != last then
		begin if cr then PUNLCR; NL; uit (a) end;
		for k:= tw step -1 until 1 do if T[k] = a then go to exit;
		PUNLCR; PUTEXT ("fout: "); PUTEXT (s); PUTEXT (" niet bewezen"); dump; EXIT;
	exit:
	end;

	integer procedure Def (LR, L); value LR, L; Boolean LR; integer L;
	begin	integer R, opw, een, twee, x;
		opw:= opwijz (OP[L]); R:= TR[opw];
		x:= ARG1[L]; Nfalse; NAMEN (x); R:= subst (x, ARG1[R], ARG2[R]);
		if NOP[opw] = 2 then begin x:= ARG2[L]; Nfalse; NAMEN (x); R:= subst (x, ARG1[R], ARG2[R]) end;
		if LR then begin een:= L; twee:= R end else begin een:= R; twee:= L end;
		testproven (een, "formule in Def", true);
		NL1; PUTEXT ("["); opuit (OP[L]); PUTEXT ("]"); PUSYM (118);
		Def:= store (twee)
	end;

	integer procedure DefLR (L); integer L; DefLR:= Def (true, L);
	integer procedure DefRL (L); integer L; DefRL:= Def (false, L);

	integer procedure Subst (x, a); value x, a; integer x, a;
	begin	integer y;
		testproven (a, "formule voor Subst", true);
		error (OP[a] != al, "formule voor Subst begint niet met A", a); test (x);
		y:= ARG1[a]; NL; PUTEXT ("substitutie van "); uit (x); PUTEXT (" voor "); uit (y);
		NL; Nfalse; NAMEN (x); Subst:= store (subst (x, y, ARG2[a]))
	end;

	procedure Nfalse;
	begin	integer k;
		for k:= -26 step 1 until -1 do N[k]:= false
	end;

	procedure NAMEN (x); value x; integer x;
	if x < 0 then N[x]:= true else
	begin	integer a2;
		NAMEN (ARG1[x]); a2:= ARG2[x];
		if a2 != 0 then NAMEN (a2)
	end;

	integer procedure subst (x, y, form); value x, y, form; integer x, y, form;
	comment Eerst Nfalse en NAMEN (x) aanroepen;
	if form > 0 then 
	begin	if OP[form] = al then error (N[ARG1[form]], "te substitueren variabele komt gebonden voor", x);
		subst:= form2 (OP[form], subst (x, y, ARG1[form]), subst (x, y, ARG2[form]))
	end	else
	subst:= if form = y then x else form;

	integer procedure Stel (a); value a; integer a;
	begin	hw:= hw + 1; NL; PUTEXT ("Stel "); Stel:= store (a);
		test (a); TBV[hw]:= 0; H[hw]:= tw
	end;

	procedure Intro (x); value x; integer x;
	begin	hw:= hw + 1; NL; PUTEXT ("Zij "); uit (x);
		PUTEXT (" een uitspraak"); onbek (x); OPW[hw]:= opw;
		H[hw]:= tw; TBV[hw]:= x
	end;

	integer procedure Terug;
	begin	integer h, Tl, x;
		h:= H[hw]; Tl:= T[tw]; x:= TBV[hw];
		if x < 0 then
		begin	opw:= OPW[hw];
			if tw > h then
			begin test (Tl); tw:= h; NL1; store (A (x, Tl)) end;
			M[x]:= false
		end	else
		begin tw:= h - 1; NL1; store (Impl (T[h], Tl)) end;
		hw:= hw - 1; Terug:= T[tw]
	end;

	procedure BEGIN;
	begin	integer kk;
		a:= -1; b:= -2; c:= -3; d:= -4; e:= -5; f:= -6; g:= -7; h:= -8; i:= -9; j:= -10;
		k:= -11; l:= -12; m:= -13; n:= -14; o:= -15; p:= -16; q:= -17; r:= -18;
		s:= -19; t:= -20; u:= -21; v:= -22; w:= -23; x:= -24; y:= -25; z:= -26;
		CODE[1]:= al; CODE[2]:= impl; NOP[1]:= NOP[2]:= 2; opw:= 2;
		last:= ow:= tw:= hw:= 0;
		for kk:= -26 step 1 until -1 do M[kk]:= false; PUNLCR
	end;

	procedure QED;
r:	if hw > 0 then begin Terug; go to r end else
	begin PUNLCR; PUTEXT ("Q.E.D."); PUNLCR end;

	comment Hier moet de band met het bewijs volgen.