Commits

Paweł Wieczorek committed 4aa3f50

*

Comments (0)

Files changed (2)

-Require Import Sets.Ensembles.
+
 Require Import Lang.
 Require Import Proof.
 Require Import List.
 Require Import Set_calculus.
 Require Import Finite_ensembles.
 Require Import Sets.Finite_sets.
+Require Import Sets.Ensembles.
 (*
  * Rozne pomocnicze
  *)
   destruct PrfT.
   apply pcInfSeqAxs_finite with T. assumption.
 Qed.
- 
+
 End ProofLemmas.
 
 
 apply H. apply union_preserves_subset. assumption. assumption.
 apply union_finite. apply pcProp_dec. assumption. assumption.
  assumption.
-Qed. 
+Qed. 
+
+
+Theorem PcDeduction: forall T p q,
+  (T |- p --> q)   <->  (T, p |- q).
+Proof.
+intros. split.
+intros.
+destruct H as [proof PrfT].
+set (proof' := (pcPrfDedu p q)::(pcPrfAx p)::proof).
+exists proof'. simpl. split. auto. split.
+Focus 2. split.
+apply Union_intror. apply In_singleton.
+split.
+apply Union_intror. apply In_singleton.
+apply PcInfSeq_superset with T. apply elem_sub_unionl.
+destruct PrfT.
+
+intros. 
+Qed.
+PDFLATEX= pdflatex
+DVILATEX= latex
+DVITOPS= dvips
+EPSTOPDF= epstopdf
+LATEX_FLAGS=
+NAME= index
+WHAT_WE_WANT= pdf
+EPSS=\
+
+
+PDFS=${EPSS:.eps=.pdf}
+.SUFFIXES: .eps.pdf .eps .pdf
+.PHONY: clean
+
+.eps.pdf: ${EPSS}
+	@echo " - converting $< to pdf format"
+	@${EPSTOPDF} $<
+
+${NAME}.pdf: ${PDFS} ${NAME}.tex
+	@for i in 1 2 3; do ${PDFLATEX} ${LATEX_FLAGS} ${NAME}.tex; done
+
+${NAME}.dvi: ${NAME}.tex
+	@for i in 1 2 3; do ${DVILATEX} ${LATEX_FLAGS} ${NAME}.tex; done
+
+${NAME}.ps: ${NAME}.dvi
+	${DVITOPS} ${NAME}.dvi
+
+
+pdf: ${NAME}.pdf
+
+dvi: ${NAME}.dvi
+
+ps: ${NAME}.ps
+
+all: ${WHAT_WE_WANT}
+
+
+clean:
+	rm -f *.aux *.log *.out *.pdf *.ps *.dvi *.toc ${PDFS}