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.
 End ProofLemmas.
 apply H. apply union_preserves_subset. assumption. assumption.
 apply union_finite. apply pcProp_dec. assumption. assumption.
+Theorem PcDeduction: forall T p q,
+  (T |- p --> q)   <->  (T, p |- q).
+intros. split.
+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.
+apply Union_intror. apply In_singleton.
+apply PcInfSeq_superset with T. apply elem_sub_unionl.
+destruct PrfT.
+PDFLATEX= pdflatex
+DVILATEX= latex
+DVITOPS= dvips
+EPSTOPDF= epstopdf
+NAME= index
+.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}
+	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
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.