righ1113

Lemma col: forall P Q:nat->Prop, (forall x:nat,P x -> False) -> (forall x:nat, (forall z:nat, (P z->Q z)) -> P x) -> forall x:nat, P x .
Proof.
intros.
apply (H0 x).
intros.
apply (H z) in H1.
tauto.
Qed.

righ1113

--
-- River
--
-- $ egison                                       4.1.3
-- > loadFile "river.egi"


--
-- Data
--

righ1113

# $ iex -S mix
# > Bf.hello |> Bf.parse([]) |> Bf.run()
defmodule Bf do
  # data
  # Module.register_attribute(__MODULE__, :hello, persist: true)
  # @hello "++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-.<.+++.------.--------.>>+.>++."
  def hello do
    '++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-.<.+++.------.--------.>>+.>++.'
  end

righ1113

--
-- 5-color
--
-- Egison Jornal Vol.2 「Egison パターンマッチによるグラフの彩色」を new syntax で書いたもの
--
-- $ egison                                       4.1.3
-- > loadFile "5color.egi"


--

righ1113

-- $ idris
-- > :l Halt
module Halt

%default total


namespace Hal
  postulate H : (f : a) -> Bool

righ1113

-- 参考記事：https://qiita.com/41semicolon/items/530c0e5e4785728f7295
--
-- $ idris
-- > :l GoedelPuzzle
module GoedelPuzzle

%default total
%hide (++)

righ1113

theory Test03
  imports Main HOL.Nat HOL.Wellfounded
begin

(*
lemma hoge220802 [simp]:
  fixes F :: "nat ⇒ bool"
  and n :: nat
  assumes a: "F n"
  (* and   b: "A ≠ F" *)

righ1113

% Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.28)
% 参考: https://qiita.com/sym_num/items/955f47de4494f4c57ba8
% 実行:
% > prolog
% ?- ['./prolog_lisp.pl'].
% ?- repl.

% :- use_module(library(history)).

%Lisp in Prolog

righ1113

『四色問題を解く。』の考察

http://hadwiger.html.xdomain.jp/

22/05/28 近況

グラフ理論の本を読んでいたら、「Hajós の構成」なるものを見つけました。
https://sites.math.washington.edu/~billey/classes/562.winter.2018/articles/GraphTheory.pdf

righ1113

-- :l Esty
module Esty

%default total
%hide fib
%hide fact

syntax "sif(" [t] "," [e] ")." [bool] = ifThenElse bool t e

namespace Fun