Sandbox

提供: Internet Web School

表組みの例

整形済のプログラムリストの挿入

nowikiを使う　　

hoe hoe

environ vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3, RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4, TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0, UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0; notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1, TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY; constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1, BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1, XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY, XREAL_0, RVSUM_1; requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE; definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, PRE_POLY,FINSET_1,CARD_1; theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1, INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1, FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1, FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2, FINSET_1,PARTFUN1, PRE_POLY, CARD_1; schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1; begin now let Humankind be finite set, Tokyoite be Subset of Humankind, Numberofhair be Function of Tokyoite,NAT ; assume LM1: card (Tokyoite) = 12*10|^6; assume LM2: for x be object st x in Tokyoite holds Numberofhair.x <= 10|^6; LM0: 10|^6 + 1 < 12*10|^6 proof 0 < 10|^6 by PREPOWER:6; then P2: 1*10|^6 < 11* 10|^6 by XREAL_1:68; P3: 1 < 10 & 2 <= 6; then 10 < 10 |^6 by PREPOWER:13; then 1 < 10 |^6 by XXREAL_0:2,P3; then 1 < 11*10|^6 by P2,XXREAL_0:2; then P4: 1*10|^6 + 1 < 1*10|^6 + 11*10|^6 by XREAL_1:8; 1*10|^6 + 11*10|^6 = (1+11)*10|^6 ; hence thesis by P4; end; LM3: card (rng Numberofhair) <= 10|^6+1 proof now let y be object ; assume y in rng Numberofhair; then consider x be object such that A1: x in Tokyoite & y=Numberofhair.x by FUNCT_2:11; Numberofhair.x <= 10|^6 by A1,LM2; then Numberofhair.x < 10|^6+1 by NAT_1:16,XXREAL_0:2; then Numberofhair.x in Segm (10|^6+1) by NAT_1:44,A1; hence y in Segm (10|^6+1) by A1; end; then A2: rng Numberofhair c= Segm (10|^6+1) by TARSKI:def 3; then card rng Numberofhair <= card Segm (10|^6+1) by NAT_1:43; then card rng Numberofhair <= card (10|^6+1) by ORDINAL1:def 17; hence card rng Numberofhair <= (10|^6+1) ; end; LM4: card (rng (Numberofhair)) < card (Tokyoite) proof reconsider N1= card (rng (Numberofhair)) as Element of NAT ; reconsider N2= card (Tokyoite) as Element of NAT ; A1: N1<=(10|^6+1) & N2=12*10|^6 by LM1,LM3; then N1 < N2 by A1,XXREAL_0:2,LM0; hence thesis ; end; EX: ex x,y be object st x in Tokyoite & y in Tokyoite & x <> y & Numberofhair.x = Numberofhair.y proof assume A1: not ( ex x,y be object st x in Tokyoite & y in Tokyoite & x <> y & Numberofhair.x = Numberofhair.y ) ; then A2: for x,y be object st x in Tokyoite & y in Tokyoite & x <> y holds Numberofhair.x <> Numberofhair.y ; A3: dom Numberofhair = Tokyoite by FUNCT_2:def 1; then for x,y be object st x in dom Numberofhair & y in dom Numberofhair & Numberofhair.x = Numberofhair.y holds x = y by A2; then Numberofhair is one-to-one by FUNCT_1:def 4; then card (dom Numberofhair) = card (rng Numberofhair) by CARD_1:70; then card (Tokyoite) = card (rng (Numberofhair)) by A3; hence contradiction by LM4; end; end;

preタグを使う　　

ここにマークアップを無効にするテキストを入力します

environ

 vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
      RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
      TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
      UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
      TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
 constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
      BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
      XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
      XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
      XREAL_0, RVSUM_1;

::---------------------------------------
:: Combined Circuit Structure of STC_TYPE0_Inter_Inter.

definition
  let x1,x2,x3,x5,x6,x7 be set;
  func STC0IIStr(x1,x2,x3,x5,x6,x7) ->
    unsplit gate`1=arity gate`2isBoolean
    non void strict non empty ManySortedSign
  equals
:: WALLACE1:def 1
    BitGFA0Str(x1,x2,x3) +* BitGFA0Str(x5,x6,x7);
end;

別ウインドウでハイパーリンク先を表示

• CAIテストのページへ（新しいWindowが開きます）

• リンク先を別ウインドウで表示[1]