Sandbox

提供: Internet Web School

(版間での差分)
 
(間の5版分が非表示)
1 行: 1 行:
 +
== 表示名を変える ==
 +
 +
*[[線形計画法（生産計画）|表示はhoeだが実体は線形計画法のページです]]
 +
 +
 +
== 表組みの例 ==
== 表組みの例 ==
16 行: 22 行:
== 整形済のプログラムリストの挿入 ==
== 整形済のプログラムリストの挿入 ==
-
=== nowikiを使う　　===
+
=== nowikiはダメっぽい　　===
<nowiki>
<nowiki>
23 行: 29 行:
</nowiki>
</nowiki>
-
<nowiki>
+
=== preタグを使う　　===
-
environ
+
-
vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
+
<pre>
-
      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,
+
</pre>
-
      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
+
<pre style="font-size:medium">
 +
少し大きな文字のテキスト
 +
</pre>
-
 
+
<pre style="font-size:large">
-
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;
+
-
 
+
-
 
+
-
 
+
-
</nowiki>
+
-
 
+
-
=== preタグを使う　　===
+
-
 
+
-
<pre>
+
-
ここにマークアップを無効にするテキストを入力します
+
</pre>
</pre>

2020年12月22日 (火) 11:06 時点における最新版

目次

表示名を変える


表組みの例

Food complements
オレンジ りんご
パン パイ
バター アイスクリーム

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

nowikiはダメっぽい　　

hoe hoe

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;

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

  • リンク先を別ウインドウで表示[1]
「http://ja.iwschool.org/wiki/Sandbox」より作成
個人用ツール