[Date Prev][Date Next] [Chronological] [Thread] [Top]

**To**:**mizar-forum@mizar.uwb.edu.pl****Subject**:**[mizar] Contradiction in Mizar 6.3.05****From**:**Piotr Rudnicki <piotr@cs.ualberta.ca>**- Date: Thu, 26 Jun 2003 18:44:14 -0600
- Content-disposition: inline
- User-agent: Mutt/1.2.5.1i

Hi: One can prove a contradiction in Mizar 6.3.05 but I guess it is not a new feature. See attached. -- Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr

VGraph-yielding MGraphSeq ODCSeq Vbooboo

:: Gilbert Lee environ vocabulary FUNCT_1, BOOLE, GRAPH_1, FINSET_1, FUNCT_4, CAT_1, NEWTON, CLUERR, RELAT_1, FINSEQ_1, GRAPH_5, RLVECT_1, ORDERS_1, PARTFUN1, PBOOLE, SCM_1, CARD_1, AMI_1, MSAFREE2, SQUARE_1, FUNCOP_1, TARSKI; notation ARYTM_0, RELAT_1, FUNCT_1, NAT_1, PBOOLE, FUNCOP_1, GRAPH_1; constructors ABIAN, GRAPH_5, SQUARE_1; clusters ARYTM_0, GRAPH_1, FUNCOP_1; requirements SUBSET, BOOLE; theorems CQC_LANG, CARD_1, GRAPH_1, SQUARE_1, TARSKI, ZFMISC_1, CARD_2, FUNCT_4, FUNCT_1, RELAT_1, FINSEQ_1, RELSET_1, FUNCT_2, REAL_1, GRAPHSP, GRAPH_5, FINSEQ_3, XBOOLE_0, AXIOMS, NAT_1, FUNCOP_1, PBOOLE; schemes NAT_1, FUNCT_1; begin definition let IT be set; attr IT is booboo means :DDDD: 1 = 0; end; definition let IT be MultiGraphStruct; redefine attr IT is finite; synonym IT is booboo; end; definition let F be ManySortedSet of NAT; attr F is Graph-yielding means :LGY: for x being set st x in rng F holds x is Graph; end; GY: now let G be Graph; set f = NAT --> G; A: dom f = NAT by FUNCOP_1:19; hence f is ManySortedSet of NAT by PBOOLE:def 3; then reconsider f as ManySortedSet of NAT; take f; thus f = NAT --> G; thus f is Graph-yielding proof let x be set; assume x in rng f; then consider y being set such that AA: y in dom f & f.y = x by FUNCT_1:def 5; f.y = G by A, AA, FUNCOP_1:13; hence x is Graph by AA; end; end; definition cluster Graph-yielding ManySortedSet of NAT; correctness proof consider G being Graph; consider f being ManySortedSet of NAT such that A: f = NAT --> G & f is Graph-yielding by GY; thus thesis by A; end; end; definition mode GraphSeq is Graph-yielding ManySortedSet of NAT; end; definition let f be GraphSeq, x be Nat; redefine func f.x -> Graph; correctness proof x in NAT; then x in dom f by PBOOLE:def 3; then f.x in rng f by FUNCT_1:12; hence f.x is Graph by LGY; end; end; definition let G be Graph; func DCSeq G -> GraphSeq equals :LDCS: NAT --> G; correctness proof consider f being ManySortedSet of NAT such that A: f = NAT --> G & f is Graph-yielding by GY; thus thesis by A; end; end; DCS: now let G be Graph, n be Nat; DCSeq G = NAT --> G by LDCS; hence (DCSeq G).n = G by FUNCOP_1:13; end; definition let G be finite Graph, n be Nat; cluster (DCSeq G).n -> booboo; correctness proof thus (DCSeq G).n is finite by DCS; end; end; consider G being finite Graph, n being Nat; ((DCSeq G).n qua set) is booboo; then contradiction by DDDD;

**Follow-Ups**:**Re: [mizar] Contradiction in Mizar 6.3.05***From:*Josef Urban <urban@ktilinux.ms.mff.cuni.cz>

- Prev by Date:
**[mizar] robustness of the Mizar system** - Next by Date:
**Re: [mizar] Contradiction in Mizar 6.3.05** - Index(es):