Paweł Wieczorek avatar 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}
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.