Finite Field
30 秒诊断
返回 NPA

模块

Mathlib.Core.Reduction

npa-mathlib

包

2

模块

63

定理

750

声明

1016

非可信 sidecar

源文本和展示 overlay 属于展示元数据。可信证据是签名证书和 checker 结果。

定理

5

定义

1

归纳类型

0

公理

0

声明

reduction_id_nat

forall (n : Nat), Nat

definition

beta_id_nat

forall (n : Nat), Nat

theorem

beta_const_nat

forall (n : Nat), forall (m : Nat), Nat

theorem

let_id_nat

forall (n : Nat), Nat

theorem

let_const_nat

forall (n : Nat), Nat

theorem

delta_id_nat

forall (n : Nat), Nat

theorem

哈希

source
sha256:53f6a264f4626ff04d6c5de4d5537e3788ea03b28c0c507c8137de1c55fbf531
certificateFile
sha256:df9ac4f4d242d488d044e5dc51b6c78402e921531d6e8d4b625257873d8d6332
export
sha256:2569ced477b19ec5058860d727cf520416e353f6fe8c682a323a605869ae7902
axiomReport
sha256:70b2d0f35f9ebfff46bdf399b80487f0c76ffd6460ab930f733af1f889d2fc65
certificate
sha256:a30a2ceacf391a9635367aa4f760ccf60431809c27f973035d0ed1dede98fd22

源文本

import Std.Nat.Basic

def reduction_id_nat :
  forall (n : Nat), Nat :=
  fun n => n

theorem beta_id_nat :
  forall (n : Nat), Nat :=
  fun n => (fun (x : Nat) => x) n

theorem beta_const_nat :
  forall (n : Nat), forall (m : Nat), Nat :=
  fun n => fun m => (fun (x : Nat) => fun (y : Nat) => x) n m

theorem let_id_nat :
  forall (n : Nat), Nat :=
  fun n => let x : Nat := n in x

theorem let_const_nat :
  forall (n : Nat), Nat :=
  fun n => let z : Nat := Nat.zero in z

theorem delta_id_nat :
  forall (n : Nat), Nat :=
  reduction_id_nat