kmx.io/prism.js/examples/prism-mizar.html

• Show log

  Commit

• Hash : 36a5fa0e
  Author :
  Date : 2019-06-30T04:19:54
  

  Known failure page (#1876) This PR adds a known failures page. This resolves #1750. The known failures are moved from the example pages. (I also updated all example pages with invalid HTML.) Some known failures were actually fixed in the meantime but never updated, so I removed a few. Those were: - Handlebars - Markdown's nested bold-italic - Smarty - Textile's "Nested styles are only partially supported" ### Screenshot <details>  </details>

Download

• examples/prism-mizar.html

• <h2>Full example</h2>
  
  <pre><code>:: Example from http://webdocs.cs.ualberta.ca/~piotr/Mizar/Dagstuhl97/
  environ
  vocabulary SCM;
  constructors ARYTHM, PRE_FF, NAT_1, REAL_1;
  notation ARYTHM, PRE_FF, NAT_1;
  requirements ARYTHM;
  theorems REAL_1, PRE_FF, NAT_1, AXIOMS, CQC_THE1;
  schemes NAT_1;
  begin
  
  P: for k being Nat
  	st for n being Nat st n &lt; k holds Fib (n+1) ≥ n
  		holds Fib (k+1) ≥ k
  proof let k be Nat; assume
  IH: for n being Nat st n &lt; k holds Fib (n+1) ≥ n;
  	per cases;
  		suppose k ≤ 1; then k = 0 or k = 0+1 by CQC_THE1:2;
  			hence Fib (k+1) ≥ k by PRE_FF:1;
  		suppose 1 &lt; k; then
  			1+1 ≤ k by NAT_1:38; then
  			consider m being Nat such that
  		A: k = 1+1+m by NAT_1:28;
  			thus Fib (k+1) ≥ k proof
  				per cases by NAT_1:19;
  				suppose S1: m = 0;
  					Fib (0+1+1+1) = Fib(0+1) + Fib(0+1+1) by PRE_FF:1
  					              = 1 + 1 by PRE_FF:1;
  					hence Fib (k+1) ≥ k by A, S1;
  				suppose m > 0; then
  					m+1 > 0+1 by REAL_1:59; then
  					m ≥ 1 by NAT_1:38; then
  				B: m+(m+1) ≥ m+1+1 by REAL_1:49;
  				C: k = m+1+1 by A, AXIOMS:13;
  				   m &lt; m+1 & m+1 &lt; m+1+1 by REAL_1:69; then
  				   m &lt; k & m+1 &lt; k by C, AXIOMS:22; then
  				D: Fib (m+1) ≥ m & Fib (m+1+1) ≥ m+1 by IH;
  				   Fib (m+1+1+1) = Fib (m+1) + Fib (m+1+1) by PRE_FF:1; then
  				   Fib (m+1+1+1) ≥ m+(m+1) by D, REAL_1:55;
  		hence Fib(k+1) ≥ k by C, B, AXIOMS:22;
  	end;
  end;
  
  for n being Nat holds Fib(n+1) ≥ n from Comp_Ind(P);</code></pre>
  

Download