COSC5100 Validity Checker Examples	1/22/2003

	EX1: (A->B->C) -> (A->(B->C))

	The number in parenthesis indicates the number of parts
	of the formula, either Anti or Cons.
	Parts in Anti are really their conjunctions while parts
	in Cons are their disjunctions, of course.

	A. Anti(0)
	   Cons(1):	(A->B->C) -> (A->(B->C))

	B. CIMP
	   Anti(1):	A->B->C
	   Cons(1):	A->(B->C)

	C. AIMP: 	2 implications (Their conjunction)
	   1.  Anti(1):	C
	       Cons(1):	A->(B->C)
	   2.  Anti(0):
	       Cons(2):	A->(B->C)
			A->B

	D. Now consider just the first implication
	       Anti(1):	C
	       Cons(1): A->(B->C)

	E. CIMP:	Anti(2):	C
					A
			Cons(1):	B->C

	F. CIMP:	Anti(3):	C
					A
					B
			Cons(1):	C

	At this time, the first implication's elimination is done.			
	So, we check if any one variable occurs in both Anti and
	Conseq.  The variable C does. So, it is valid.

	Now, we check go ahead to check for the second implication.
	Of course, if the first implication were not valid, we would
	be done as the whole formula is found not to be VALID.

	G.     Anti(0)
	       Cons(2):			A->(B->C)
					A->B
	   CIMP:  	Anti(1):	A
			Cons(2):	B->C
					A->B

	H. CIMP:	Anti(2):	A
					B
			Cons(2):	C
					A->B

	I. CIMP:	Anti(3):	A
					B
					A
			Cons(2):	C
					B

	Now, the second implication is done.
	And, as we check to see if a variable occurs in both Anti
	and Cons, it is 'B' that does occur in both.

	As all implications (2 of them, in this case) are Valid,
	the original formula is found to be valid.

	EX2:	(A->B) AND (B->C) -> (A->C)

	A. Anti(0)
	   Cons(1):	(A->B) AND (B->C) -> (A->C)

	B. CIMP:	
		Anti(1):	(A->B) AND (B->C)
		Cons(1):	A->C

	C. AAND:
		Anti(2):	A->B
				B->C
		Cons(1):	A->C

	D. AIMP: 
	   We get 2 implications.

	   1.	Anti(2):	B
				B->C
		Cons(1):	A->C

	   2.	Anti(1):	B->C
		Cons(2):	A->C
				A

	E. Again, we consider the first implication:
		Anti(2):	B
				B->C
		Cons(1):	A->C

	F. AIMP:
	   So, we get two implications:
		
		1-1.	Anti(2):	B
					C
			Cons(1):	A->C

		1-2.	Anti(1):	B
			Cons(2):	A->C
					B	
	G. Consider 1-1 above.
			Anti(2):	B
					C
			Cons(1):	A->C

		G1.	CIMP:
			Anti(3):	B
					C
					A
			Cons(1):	C
		G2.	Now this implication is over and 
			it is VALID

	H. Now consider 1-2 above.
			Anti(1):	B
			Cons(2):	A->C
					B
		H1.	CIMP:
			Anti(2):	B
					A
			Cons(2):	C
					B	
		H2.	Now this implication is over and VALID.

	I. Now consider the second implication of step D above.
		Anti(1): 	B->C
		Cons(2):	A->C
		         	A
	   CIMP:  (Although it is also a case of AIMP)
			Anti(2):	B->C
					A
			Cons(2):	C
					A

	J. AIMP: So we get 2 implications.
		2-1:	Anti(2):	C
					A
			Cons(2):	C
					A
		2-2:	Anti(1):	A
			Cons(3):	C
					A
					B
	K. From inspection, we see that both implications, 2-1 and 2-2,
	   are done and they are both VALID.
	   So, the original formula, EX2, is VALID, as we expect.