Sandbox - 変更履歴

2020年12月22日 (火) 10:57 における Moderator による編集

Moderator — Tue, 22 Dec 2020 10:57:17 GMT

←前の版		2020年12月22日 (火) 10:57時点における版
1 行:		1 行:
-	== ~~MathJaxの表示テスト~~ ==	+	== 表示名を変える ==
-		+
-	~~ある製造会社があって, $x$ と $y$ という２種類の製品の製造販売をしている.~~	+
-	~~これらを製造するには, 原材料$A$，$B$，$C$が必要で, $x$, $y$をそれぞれ1単位当~~	+
-	~~たり造るのに必要な量と, 使用できる在庫量が下の表のように決まっている．~~	+

		+	*[[線形計画法（生産計画）\|表示はhoeだが実体は線形計画法のページです]]

2020年12月22日 (火) 09:30 における Moderator による編集

Moderator — Tue, 22 Dec 2020 09:30:51 GMT

←前の版		2020年12月22日 (火) 09:30時点における版
1 行:		1 行:
		+	== MathJaxの表示テスト ==
		+
		+	ある製造会社があって, $x$ と $y$ という２種類の製品の製造販売をしている.
		+	これらを製造するには, 原材料$A$，$B$，$C$が必要で, $x$, $y$をそれぞれ1単位当
		+	たり造るのに必要な量と, 使用できる在庫量が下の表のように決まっている．
		+
		+
		+
		+
	== 表組みの例 ==		== 表組みの例 ==

76 行:		85 行:

	*<span class="pops"> リンク先を別ウインドウで表示[http://mizar.org/version/current/html/alg_1.html] </span>		*<span class="pops"> リンク先を別ウインドウで表示[http://mizar.org/version/current/html/alg_1.html] </span>
-
-	~~== MathJaxの表示テスト ==~~
-
-	~~ある製造会社があって, $x$ と $y$ という２種類の製品の製造販売をしている.~~
-	~~これらを製造するには, 原材料$A$，$B$，$C$が必要で, $x$, $y$をそれぞれ1単位当~~
-	~~たり造るのに必要な量と, 使用できる在庫量が下の表のように決まっている．~~

2020年12月22日 (火) 09:29 における Moderator による編集

Moderator — Tue, 22 Dec 2020 09:29:39 GMT

←前の版		2020年12月22日 (火) 09:29時点における版
76 行:		76 行:

	*<span class="pops"> リンク先を別ウインドウで表示[http://mizar.org/version/current/html/alg_1.html] </span>		*<span class="pops"> リンク先を別ウインドウで表示[http://mizar.org/version/current/html/alg_1.html] </span>
		+
		+	== MathJaxの表示テスト ==
		+
		+	ある製造会社があって, $x$ と $y$ という２種類の製品の製造販売をしている.
		+	これらを製造するには, 原材料$A$，$B$，$C$が必要で, $x$, $y$をそれぞれ1単位当
		+	たり造るのに必要な量と, 使用できる在庫量が下の表のように決まっている．

2020年12月1日 (火) 00:32 における Moderator による編集

Moderator — Tue, 01 Dec 2020 00:32:38 GMT

←前の版		2020年12月1日 (火) 00:32時点における版
26 行:		26 行:

	<pre>		<pre>
-	~~ここにマークアップを無効にするテキストを入力します~~	+	ここにマークアップを無効にするテキストを入力します．
		+	</pre>
		+
		+	<pre style="font-size:medium">
		+	少し大きな文字のテキスト
		+	</pre>
		+
		+	<pre style="font-size:large">
		+	かなり大きな文字のテキスト
	</pre>		</pre>

Moderator: /* 整形済のプログラムリストの挿入 */

Moderator — Mon, 30 Nov 2020 05:42:52 GMT

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

←前の版		2020年11月30日 (月) 05:42時点における版
16 行:		16 行:
	== 整形済のプログラムリストの挿入 ==		== 整形済のプログラムリストの挿入 ==

-	=== ~~nowikiを使う~~　　===	+	=== nowikiはダメっぽい　　===

	<nowiki>		<nowiki>

Moderator: /* 整形済のプログラムリストの挿入 */

Moderator — Mon, 30 Nov 2020 05:40:00 GMT

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

←前の版		2020年11月30日 (月) 05:40時点における版
21 行:		21 行:
	hoe		hoe
	hoe		hoe
-	~~</nowiki>~~
-
-	~~<nowiki>~~
-	~~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: 110\|^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: 110\|^6 + 1 < 110\|^6 + 11*10\|^6 by XREAL_1:8;~~
-	~~110\|^6 + 1110\|^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>		</nowiki>

2020年11月30日 (月) 05:38 における Moderator による編集

Moderator — Mon, 30 Nov 2020 05:38:39 GMT

←前の版		2020年11月30日 (月) 05:38時点における版
183 行:		183 行:
	<pre>		<pre>
	ここにマークアップを無効にするテキストを入力します		ここにマークアップを無効にするテキストを入力します
		+	</pre>
		+
		+	<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;
	</pre>		</pre>

Moderator: /* nowikiを使う　　 */

Moderator — Mon, 30 Nov 2020 05:37:57 GMT

nowikiを使う　　

←前の版		2020年11月30日 (月) 05:37時点における版
17 行:		17 行:

	=== nowikiを使う　　===		=== nowikiを使う　　===
		+
		+	<nowiki>
		+	hoe
		+	hoe
		+	</nowiki>
		+
	<nowiki>		<nowiki>
	environ		environ

Moderator: /* nowikiを使う　　 */

Moderator — Mon, 30 Nov 2020 04:27:24 GMT

nowikiを使う　　

←前の版		2020年11月30日 (月) 04:27時点における版
18 行:		18 行:
	=== nowikiを使う　　===		=== nowikiを使う　　===
	<nowiki>		<nowiki>
-	~~ここにマークアップを無効にするテキストを入力します~~	+	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: 110\|^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: 110\|^6 + 1 < 110\|^6 + 11*10\|^6 by XREAL_1:8;
		+	110\|^6 + 1110\|^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>		</nowiki>

2020年11月30日 (月) 03:28 における Moderator による編集

Moderator — Mon, 30 Nov 2020 03:28:15 GMT

←前の版		2020年11月30日 (月) 03:28時点における版
46 行:		46 行:
	*<span class="pops"> [[cai_ja:EDUPHI00010001\|CAIテストのページへ（新しいWindowが開きます）]] </span>		*<span class="pops"> [[cai_ja:EDUPHI00010001\|CAIテストのページへ（新しいWindowが開きます）]] </span>

-	*<span class="pops"> [http://mizar.org/version/current/html/alg_1.html] </span>	+	*<span class="pops"> リンク先を別ウインドウで表示[http://mizar.org/version/current/html/alg_1.html] </span>

Sandbox - 変更履歴

2020年12月22日 (火) 10:57 における Moderator による編集

2020年12月22日 (火) 09:30 における Moderator による編集

2020年12月22日 (火) 09:29 における Moderator による編集

2020年12月1日 (火) 00:32 における Moderator による編集

Moderator: /* 整形済のプログラムリストの挿入 */

Moderator: /* 整形済のプログラムリストの挿入 */

2020年11月30日 (月) 05:38 における Moderator による編集

Moderator: /* nowikiを使う */

Moderator: /* nowikiを使う */

2020年11月30日 (月) 03:28 における Moderator による編集

Moderator: /* nowikiを使う　　 */

Moderator: /* nowikiを使う　　 */