[mizar] Contradiction in Mizar 6.3.05

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

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;