0

合成関数

14
0

hbhb bbk hbhb bbk

imp

imp a b:=a b

tran

tran U R:=x y z:U,R x yR y zR x z

tran imp

      Require Import Utf8.

Set Implicit Arguments.

Definition imp a b:=a → b.

Definition tran U R:=
 ∀x y z:U,R x y → R y z → R x z.

Fact Biden:tran imp.
VOTE!
    
投稿日:20201125
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中