We are currently working on new rules for what content should and shouldn't be allowed on this website, and are looking for feedback! See Esolang:2026 topicality proposal to view and give feedback on the current draft.

Тест на терпение

From Esolang
Jump to navigation Jump to search
Тест на терпение
Paradigm(s) Declarative
Designed by User:Hakerh400
Appeared in 2020
Computational class Not applicable
Major implementations Implementation in JavaScript
File extension(s) .txt

Тест на терпение is an interactive theorem prover invented by User:Hakerh400 in 2020.

Overview

This is a theorem prover inspired by Isabelle/HOL. It uses simple type theory. All types are inhabited. There are no builtin axioms. There is no meta-level and term-level, unlike in Isabelle. Everything is defined on the term level.

The builtin logic knows only about the following concepts:

  • Proposition type (boolean)
  • Function type
  • Lambda expression
  • Universal quantifier
  • Implication
  • Equality

Syntax

Source code consists of directives. The language recognizes the following directives:

  • spacing - Specify whitespace information for pretty-printer
  • type - Declare a type
  • const - Declare a value
  • def - Define a value
  • meta - Associate an identifier to one of the builtin concepts
  • axiom - Specify an axiom
  • lemma - Specify a lemma (theorem) and verify its proof

Tactics

There are a lot of tactics that can be used in proof mode. We are not going to document all of them. Not even a single one.

Example

We define some of the basic data structures and prove some theorems about them. 

spacing ( ⟹ ) 1 1 1
spacing ( ⟶ ) 1 1 1
spacing (THE) 0 1 0

type ( ⟹ ) 2 [infixr 25]
type bool  0

const True  :: bool
const False :: bool

const (∀)   [binder]    :: ('a  ⟹  bool)  ⟹  bool
const (THE) [binder]    :: ('a  ⟹  bool)  ⟹  'a
const ( ⟶ ) [infixr 25] :: bool  ⟹  bool  ⟹  bool
const (=)   [infixl 50] :: 'a  ⟹  'a  ⟹  bool

meta bool   bool
meta arrow  ( ⟹ )
meta lambda (λ)
meta uni    (∀)
meta imp    ( ⟶ )
meta eq     (=)

axiom true:     True
axiom bool_dif: ∀P. True = False  ⟶  P
axiom bool_ind: ∀P. P True  ⟶  P False  ⟶  (∀) P

axiom refl: ∀a. a = a
axiom sub:  ∀P a b. a = b  ⟶  P a  ⟶  P b
axiom ext:  ∀f g. (∀a. f a = g a)  ⟶  f = g
axiom the:  ∀a. (THE b. b = a) = a

lemma psub: ∀P Q. P = Q  ⟶  P  ⟶  Q
  - sub[λx. x] 1 2 %

lemma eq_com: ∀a b. a = b  ⟶  b = a
  - sub[λx. x = a] 1 refl %

lemma eq_tran: ∀a c b. a = b  ⟶  b = c  ⟶  a = c
  - eq_com 1*
  - sub[λx. x = b] 1 2 %

lemma subr: ∀P a b. b = a  ⟶  P a  ⟶  P b
  - eq_com 1*
  - sub 1 2 %

lemma psubr: ∀P Q. Q = P  ⟶  P  ⟶  Q
  - subr[λx. x] 1 2 %

lemma fun_cong: ∀f g a. f = g  ⟶  f a = g a
  - sub[λx. a c = x c] 1 refl %

lemma fun_cong2: ∀f g a b. f = g  ⟶  f a b = g a b
  - fun_cong 1 [c]
  - fun_cong 1 %

lemma arg_cong: ∀f a b. a = b  ⟶  f a = f b
  - sub[λx. a b = a x] 1 refl %

lemma cong: ∀f g a b. f = g  ⟶  a = b  ⟶  f a = g b
  - fun_cong 1 [c]
  - sub[λx. a c = b x] 1 2 %

lemma imp_refl: ∀P. P  ⟶  P
  - 1 %

lemma lk_lem1: ∀P Q. P  ⟶  Q  ⟶  P
  - 1 %

lemma lk_lem2: ∀P Q R. (P  ⟶  Q  ⟶  R)  ⟶  (P  ⟶  Q)  ⟶  P  ⟶  R
  - 2* 3+
  - 1 3 2 %

const undefined :: 'a

def (¬)   [prefix 70]: λP. P  ⟶  False
def (∧)   [infixl 35]: λP Q. ¬(P  ⟶  ¬Q)
def (∨)   [infixl 30]: λP Q. ¬P  ⟶  Q

lemma not_def: ∀P. ¬ P = (P  ⟶  False)
  - fun_cong ¬_def %

lemma conj_def: ∀P Q. (P ∧ Q) = ¬(P  ⟶  ¬ Q)
  - fun_cong2 ∧_def %

lemma disj_def: ∀P Q. (P ∨ Q) = (¬P  ⟶  Q)
  - fun_cong2 ∨_def %

lemma falI: ∀P. P  ⟶  ¬P  ⟶  False
  - psub not_def 2 1 %

lemma falE: ∀P. False  ⟶  P
  - bool_ind[λx. x] true 1 %

lemma notI: ∀P. (P  ⟶  False)  ⟶  ¬P
  - eq_com not_def
  - psub 2 1 %

lemma notI2: ∀P. P  ⟶  ¬¬P
  - falI 1
  - notI 1 %

lemma nfalse: ¬False
  - notI imp_refl %

lemma true_neq_false: ¬ (True = False)
  - notI %
  - psub 1 true %

lemma bool_exh: ∀a P. (a = True  ⟶  P)  ⟶  (a = False  ⟶  P)  ⟶  P
  - bool_ind[λx. a = x  ⟶  b] 1 2 refl %

lemma eq_truE: ∀P. P = True  ⟶  P
  - psubr 1 true %

lemma eq_falE: ∀P. P = False  ⟶  ¬P
  - psub 1
  - notI 1 %

lemma falE2: ∀P Q. P  ⟶  ¬P  ⟶  Q
  - falI 1 2
  - falE 1 %

lemma notE: ∀P. ¬¬P  ⟶  P
  - bool_exh[a, a] %
  - eq_truE 2 %
  - eq_falE 2
  - falE2 2 1 %

lemma conjI: ∀P Q. P  ⟶  Q  ⟶  P ∧ Q
  - psubr conj_def %
  - notI %
  - 3 1
  - falI 1 2 %

lemma imp_swap: ∀P Q R. (P  ⟶  Q  ⟶  R)  ⟶  Q  ⟶  P  ⟶  R
  - 1 3 2 %

lemma falE2_swap: ∀P Q. ¬P  ⟶  P  ⟶  Q
  - falE2 2 1 %

lemma notE2: ∀P. (¬P  ⟶  False)  ⟶  P
  - notI 1
  - notE 1 %

lemma conjE1: ∀P Q. P ∧ Q  ⟶  P
  - psub conj_def 1
  - notE2 %
  - falE2_swap 2
  - falI 2 1 %

lemma cpos_pp: ∀Q P. (P  ⟶  Q)  ⟶  ¬Q  ⟶  ¬P
  - notI %
  - 1 3
  - falI 2 1 %

lemma cpos_pn: ∀Q P. (P  ⟶  ¬Q)  ⟶  Q  ⟶  ¬P
  - notI %
  - 1 3
  - falI 1 2 %

lemma cpos_np: ∀Q P. (¬P  ⟶  Q)  ⟶  ¬Q  ⟶  P
  - notE2 %
  - 1 3
  - falI 2 1 %

lemma cpos_nn: ∀Q P. (¬P  ⟶  ¬Q)  ⟶  Q  ⟶  P
  - notE2 %
  - 1 3
  - falI 1 2 %

lemma conjE2: ∀P Q. P ∧ Q  ⟶  Q
  - psub conj_def 1
  - notE2 %
  - lk_lem1 2
  - falI 2 1 %

lemma conj_com: ∀P Q. P ∧ Q  ⟶  Q ∧ P
  - conjE1 1+
  - conjE2 1
  - conjI 2 1 %

lemma disjI1: ∀P Q. P  ⟶  P ∨ Q
  - psubr disj_def %
  - falE2 1 2 %

lemma disjI2: ∀P Q. P  ⟶  Q ∨ P
  - psubr disj_def %
  - 1 %

lemma imp_tran: ∀P R Q. (P  ⟶  Q)  ⟶  (Q  ⟶  R)  ⟶  P  ⟶  R
  - 1 3
  - 1 2 %

lemma split: ∀P Q. (P  ⟶  Q)  ⟶  (¬P  ⟶  Q)  ⟶  Q
  - bool_exh[a] %
  - eq_truE 3
  - 1 3 %
  - eq_falE 3
  - 2 3 %

lemma disjE: ∀P Q R. P ∨ Q  ⟶  (P  ⟶  R)  ⟶  (Q  ⟶  R)  ⟶  R
  - psub disj_def 1*
  - split[a] %
  - 2 4 %
  - 1 4
  - 2 3 %

lemma disj_com: ∀P Q. P ∨ Q  ⟶  Q ∨ P
  - disjE 1 %
  - disjI2 1 %
  - disjI1 1 %

lemma eq_truI: ∀P. P  ⟶  P = True
  - bool_exh[a] %
  - 2 %
  - eq_falE 2
  - falE2 1 2 %

lemma eq_falI: ∀P. ¬P  ⟶  P = False
  - bool_exh[a] %
  - eq_truE 2
  - falE2 2 1 %
  - 2 %

lemma eq_tran1: ∀a b c. a = c  ⟶  b = c  ⟶  a = b
  - eq_com 2
  - eq_tran 1 2 %

lemma eq_tran2: ∀a b c. c = a  ⟶  c = b  ⟶  a = b
  - eq_com 1*
  - eq_tran 1 2 %

lemma imp_eq_p: ∀P Q. P  ⟶  Q  ⟶  P = Q
  - eq_truI 1*
  - eq_truI 2
  - eq_tran1 1 2 %

lemma eq_notI: ∀P Q. P = Q  ⟶  ¬P = ¬Q
  - arg_cong 1 %

lemma ntru_eq_fal: ¬True = False
  - eq_falI %
  - notI2 true %

lemma nfal_eq_tru: ¬False = True
  - eq_truI nfalse %

lemma add_sup: ∀Q P. P  ⟶  Q  ⟶  P
  - 1 %

lemma not2_eq: ∀P. ¬¬P = P
  - split[a] %
  - imp_eq_p %
  - notI2 1 %
  - 1 %
  - eq_falI 1
  - subr[λx. ¬¬x = x] 1 %
  - subr[λx. ¬x = False] nfal_eq_tru %
  - ntru_eq_fal %

lemma eq_notE: ∀P Q. ¬P = ¬Q  ⟶  P = Q
  - arg_cong[(¬)] 1
  - sub[λx. x = ¬¬b] not2_eq 1
  - sub[λx. a = x] not2_eq 1 %

lemma imp_eq_n: ∀P Q. ¬P  ⟶  ¬Q  ⟶  P = Q
  - imp_eq_p 1 2
  - eq_notE 1 %

lemma imp_neq: ∀P Q. P  ⟶  ¬Q  ⟶  ¬ (P = Q)
  - notI %
  - eq_truI 1*
  - eq_falI 2*
  - sub[λx. x = b] 1 3
  - eq_tran 2 1
  - bool_dif 1 %

lemma excm: ∀P. P ∨ ¬P
  - split[a] %
  - disjI1 1 %
  - disjI2 1 %

lemma not_P_and_not_P: ∀P. ¬(P ∧ ¬P)
  - notI %
  - conjE1 1+
  - conjE2 1
  - falI 1 2 %

lemma iffI: ∀P Q. (P  ⟶  Q)  ⟶  (Q  ⟶  P)  ⟶  P = Q
  - split[a] %
  - 1 3+
  - imp_eq_p 2 3 %
  - cpos_pp 2 3+
  - imp_eq_n 2 3 %

lemma iffE1: ∀P Q. P = Q  ⟶  P  ⟶  Q
  - psub 1 2 %

lemma iffE2: ∀P Q. Q = P  ⟶  P  ⟶  Q
  - psubr 1 2 %

lemma conj_assoc: ∀P Q R. ((P ∧ Q) ∧ R) = (P ∧ (Q ∧ R))
  - iffI %
  - conjE1 1+
  - conjE1 2+
  - conjE2 2
  - conjE2 1
  - conjI 2 3
  - conjI 1 2 %
  - conjE1 1+
  - conjE2 1
  - conjE1 2+
  - conjE2 2
  - conjI 1* 2
  - conjI 1 2 %

lemma disj_assoc: ∀P Q R. ((P ∨ Q) ∨ R) = (P ∨ (Q ∨ R))
  - iffI %
  - disjE 1 %
  - disjE 1 %
  - disjI1 1 %
  - disjI1 1
  - disjI2 1 %
  - disjI2 1
  - disjI2 1 %
  - disjE 1 %
  - disjI1 1
  - disjI1 1 %
  - disjE 1 %
  - disjI2 1
  - disjI1 1 %
  - disjI2 1 %

lemma uni_swap: ∀P. (∀a b. P a b)  ⟶  (∀a b. P b a)
  - 1 %

lemma not_P_eq_not_P: ∀P. ¬(P = ¬P)
  - notI %
  - split[a] %
  - psub 1 2+
  - falI 1 2 %
  - psubr 1* 2+
  - falI 1 2 %

lemma eq_com_eq: ∀P Q. (P = Q) = (Q = P)
  - iffI %
  - eq_com 1 %
  - eq_com 1 %

lemma eq_tru_eq_P: ∀P. (P = True) = P
  - iffI %
  - eq_truE 1 %
  - eq_truI 1 %

lemma eq_fal_eq_not_P: ∀P. (P = False) = ¬P
  - iffI %
  - eq_falE 1 %
  - eq_falI 1 %

lemma eq_PQQ_P: ∀P Q. (P = Q) = Q  ⟶  P
  - notE2 %
  - eq_falI 2
  - sub[λx. (x = b) = b] 2 1
  - sub[λx. x = b, False = b, b = False] eq_com_eq 1
  - sub[λx. x = b, b = False, ¬b] eq_fal_eq_not_P 1
  - eq_com 1
  - falI 1 not_P_eq_not_P %

lemma eq_assoc: ∀P Q R. ((P = Q) = R) = (P = (Q = R))
  - iffI %
  - iffI %
  - iffI %
  - imp_eq_p 2 3
  - iffE1 1 2 %
  - iffE2 1* 3
  - iffE1 1 2 %
  - subr[λx. (a = b) = x] 2 1
  - eq_PQQ_P 1 %
  - iffI %
  - sub[λx. a = x, b = c, c = b] eq_com_eq 1*
  - eq_com 1*
  - sub[λx. (c = b) = x] 2 1
  - eq_PQQ_P 1 %
  - iffI %
  - iffE1 1* 3
  - iffE2 1 2 %
  - imp_eq_p 3 2
  - iffE2 1 2 %

lemma ind_imp_exh: ∀A B. (∀P x. P A  ⟶  P B  ⟶  P x)  ⟶  ∀y. y = A ∨ y = B
  - 1[λx. x = a ∨ x = b] %
  - disjI1 refl %
  - disjI2 refl %

def inj: λf. ∀a b. f a = f b  ⟶  a = b

lemma inj_def1: ∀f. inj f = ∀a b. f a = f b  ⟶  a = b
  - fun_cong inj_def %

def (∃) [binder]: λP. ¬∀a. ¬P a

lemma eta: ∀f. (λa. f a) = f
  - ext %
  - refl %

lemma exi_def: ∀P. (∃a. P a) = ¬∀a. ¬P a
  - fun_cong ∃_def [a]
  - imp_swap eq_tran 1 %
  - arg_cong %
  - eta %

lemma dmrg_pc: ∀P Q. P ∧ Q  ⟶  ¬(¬P ∨ ¬Q)
  - notI %
  - disjE 2 %
  - conjE1 1
  - falI 2 1 %
  - conjE2 1
  - falI 2 1 %

lemma dmrg_nc: ∀P Q. ¬(P ∧ Q)  ⟶  ¬P ∨ ¬Q
  - split[a] %
  - disjI2 %
  - notI %
  - conjI 2 3
  - falI 2 1 %
  - disjI1 2 %

lemma dmrg_pd: ∀P Q. P ∨ Q  ⟶  ¬(¬P ∧ ¬Q)
  - cpos_pn dmrg_pc %
  - subr[λx. x ∨ ¬¬b] not2_eq %
  - subr[λx. a ∨ x] not2_eq 1 %

lemma dmrg_nd: ∀P Q. ¬(P ∨ Q)  ⟶  ¬P ∧ ¬Q
  - cpos_np dmrg_nc %
  - subr[λx. ¬(x ∨ ¬¬b)] not2_eq %
  - subr[λx. ¬(a ∨ x)] not2_eq 1 %

lemma dmrg_pu: ∀P. (∀a. P a)  ⟶  ¬∃a. ¬P a
  - imp_swap cpos_pn[∀b. a b] {1}1 %
  - psub exi_def[λx. ¬a x] 1
  - imp_swap cpos_pp 1 %
  - 1 [b]
  - psubr not2_eq 1 %

lemma dmrg_nu: ∀P. ¬(∀) P  ⟶  ∃a. ¬P a
  - subr[λx. ¬(∀) x] eta 1
  - psubr exi_def [λx. ¬a x] %
  - imp_swap cpos_pp 1 %
  - 1 [b]
  - psub not2_eq 1 %

lemma dmrg_pe: ∀P. (∃a. P a)  ⟶  ¬∀a. ¬P a
  - psub exi_def 1 %

lemma dmrg_ne: ∀P. ¬(∃) P  ⟶  ∀a. ¬P a
  - imp_swap cpos_pp 1 %
  show [a = λx. a x]
  sub 2
  - psubr exi_def %
  - notI %
  - falI 1 2 %
  - ext %
  - refl %

lemma eq_not2: ∀P. ¬¬P = P
  - not2_eq %

lemma eta1: ∀P f. P f = (λx y. y) ((∀) P) P (λx. f x)
  - arg_cong %
  - ext %
  - refl %

lemma exiI: ∀a P. P a  ⟶  (∃) P
  - psubr eta1 %
  - notE2 %
  - dmrg_ne 2
  - falI 1 2 %

lemma exiE: ∀P Q. (∃) P  ⟶  (∀b. P b  ⟶  Q)  ⟶  Q
  - psub eta1 1*
  - psub exi_def 1*
  - imp_swap cpos_np 1 %
  - imp_swap cpos_pp 2 %
  - 1 2 %

lemma inj_comb_K: inj (λa b. a)
  - psubr inj_def1 %
  - fun_cong 1 %

lemma inj_not_impl_inj2: ∃f. inj f ∧ ∃a. ¬inj (f a)
  - exiI[λx y. x] %
  - conjI %
  - inj_comb_K %
  - exiI[True] %
  - notI %
  - psub inj_def1 1 [True, False] refl
  - bool_dif 1 %

lemma inj_not_impl_inj2': ¬(∀f. inj f  ⟶  ∀a. inj (f a))
  - notI %
  - 1 [λx y. x, True]
  - 1 inj_comb_K
  - psub inj_def1 1 [True, False] refl
  - bool_dif 1 %

lemma Paa_eq_Pab: ∀P. (∀a. P a a) = (∀a b. a = b  ⟶  P a b)
  - iffI %
  - 1* [b]
  - sub[λx. a b x] 2 1 %
  - 1 [b, b] refl %

lemma fgaa_eq_fgab: ∀f g. (∀a. f a = g a)  ⟶  (∀a b. a = b  ⟶  f a  ⟶  g b)
  - psub Paa_eq_Pab[λx y. a x = b y] {1}1* 2
  - psub 1 2 %

lemma fgaa_eq_ffab: ∀f g. (∀a. f a = g a)  ⟶  (∀a b. a = b  ⟶  f a  ⟶  f b)
  - arg_cong 2
  - psub 3 2 %

lemma fgab_imp_eq_fg: ∀f g. (∀a b. a = b  ⟶  f a = g b) = (f = g)
  - iffI %
  - psubr Paa_eq_Pab [λx y. a x = b y] {2}1
  - ext {1}1 %
  - cong 1 2 %

lemma uni_exi: ∀P. (∀) P  ⟶  (∃) P
  - psub eta1 1
  - exiI[undefined] %
  - 1 %

lemma exi_uni: ∀P. (∀a b. P a = P b)  ⟶  (∃) P  ⟶  (∀) P
  - exiE 2 %
  - psubr eta1 %
  - psub 1 2 %

def ∃! [binder]: λP. (∃a. P a) ∧ (∀a b. P a  ⟶  P b  ⟶  a = b)

lemma uniq_def: ∀P. (∃!a. P a) = ((∃a. P a) ∧ (∀a b. P a  ⟶  P b  ⟶  a = b))
  - fun_cong ∃!_def [a]
  - imp_swap eq_tran 1 %
  - arg_cong %
  - ext %
  - refl %

lemma uniqI: ∀P. (∃) P  ⟶  (∀a b. P a  ⟶  P b  ⟶  a = b)  ⟶  (∃!) P
  - psub eta1 1*
  - psubr eta1 %
  - psubr uniq_def %
  - conjI 1 {2}2 %

lemma uniqE': ∀P a. P a  ⟶  (∀c d. P c  ⟶  P d  ⟶  c = d)  ⟶  P = λx. a = x
  - ext %
  - iffI %
  - 2 1 3 %
  - arg_cong 3
  - psub 3 1 %

lemma eq_equiv_com: (=) = (λx y. y = x)
  - ext %
  - ext %
  - eq_com_eq %

lemma uniqE: ∀P. (∃!) P  ⟶  P ((THE) P)
  - psub eta1 1
  - psub uniq_def 1
  - conjE1 1+
  - conjE2 1
  - exiE 1 %
  - uniqE' 2+ {2}1+
  - subr[λx. x ((THE) x), λx. b = x, a] %
  - 3 %
  - eq_com %
  - subr[λx. (THE y. x b y) = b] eq_equiv_com %
  - the %

type nat 0

const 0     :: nat
const Suc   :: nat  ⟹  nat

const Suc⁻¹ :: nat  ⟹  nat
axiom Suc_inj1: ∀a. Suc⁻¹ (Suc a) = a

axiom nat_dif: ∀n. ¬(0 = Suc n)
axiom nat_ind: ∀P. P 0  ⟶  (∀n. P n  ⟶  P (Suc n))  ⟶  (∀) P

lemma Suc_inj: ∀a b. Suc a = Suc b  ⟶  a = b
  - arg_cong 1 [Suc⁻¹]
  - eq_tran2 Suc_inj1 1
  - eq_com 1
  - eq_tran2 Suc_inj1 1
  - eq_com 1 %

def (<)  [infixl 50]: λa b. ∃f. f 0 = Suc a ∧ (∀c. f (Suc c) = Suc (f c)) ∧ ∃d. f d = b
def (<=) [infixl 50]: λa b. a < b ∨ a = b

lemma lt_def: ∀a b. (a < b) = ∃f. f 0 = Suc a ∧ (∀c. f (Suc c) = Suc (f c)) ∧ ∃d. f d = b
  - fun_cong2 <_def %

lemma lte_def: ∀a b. (a <= b) = (a < b ∨ a = b)
  - fun_cong2 <=_def %

lemma lt_simp1: ∀a. 0 < Suc a
  - nat_ind[#..a] %
  - psubr lt_def %
  - exiI[Suc] %
  - conjI %
  - conjI %
  - refl %
  - refl %
  - exiI[0] %
  - refl %
  - psub lt_def 1
  - psubr lt_def %
  - exiE 1 %
  - exiI[a] %
  - conjE1 1+
  - conjE1 2+
  - conjE2 2
  - conjE2 1
  - conjI %
  - conjI %
  - 1 %
  - 2 %
  - exiE 3 %
  - exiI[Suc c] %
  - eq_tran 2 %
  - arg_cong 2 %

def id: λx. x

lemma id_def1: ∀a. id a = a
  - fun_cong id_def %

lemma not2_equiv_id: (λx. ¬¬x) = id
  - ext %
  - subr[λx. x = id a] not2_eq %
  - eq_com id_def1 %

lemma dmrg_pu1: ∀P. (∀a. ¬P a)  ⟶  ¬(∃a. P a)
  - dmrg_pu[λx. ¬a x] {1}1
  - sub[λx. ¬(∃b. x (a b))] not2_equiv_id 1
  - imp_swap cpos_pp 1 %
  - exiE[λx. a x] 1 %
  - exiI[b] %
  - psubr id_def1 %
  - 1 %

lemma lt_simp2: ∀a. ¬(a < 0)
  - notI %
  - psub lt_def 1
  - exiE[#1.10.b] 1 %
  - conjE1 1+
  - conjE1 2+
  - conjE2 2
  - conjE2 1
  - falI 3 %
  - dmrg_pu1[λx. b x = 0] %
  - nat_ind[λx. ¬(b x = 0)] %
  - notI %
  - eq_tran2 3 1
  - falI 2 nat_dif %
  - notI %
  - eq_tran2 4 2
  - falI 3 nat_dif %

def pred: λa. THE b. a = Suc b

lemma pred_def1: ∀a. pred a = THE b. a = Suc b
  - fun_cong pred_def %

lemma nat_exh1: ∀a P. (a = 0  ⟶  P)  ⟶  ((∃b. a = Suc b)  ⟶  P)  ⟶  P
  - nat_ind[λa. (a = 0  ⟶  b)  ⟶  ((∃b. a = Suc b)  ⟶  b)  ⟶  b, a] %
  - 3 refl %
  - 5 %
  - exiI[c] %
  - refl %
  - 1 3 %
  - 2 3 %

lemma uniq_eq: ∀a. ∃!b. b = a
  - uniqI[λx. x = a] %
  - exiI[a] %
  - refl %
  - eq_tran1 1 2 %

lemma suc_uniq: ∀a b. a = Suc b  ⟶  ∃!c. a = Suc c
  - uniqI[#.10.c] %
  - exiI[b] %
  - 1 %
  - eq_tran2 2 3
  - Suc_inj 2 %

lemma inj_def_eq: ∀f. inj f = (∀a b. (f a = f b) = (a = b))
  - iffI %
  - psub inj_def1 1
  - iffI %
  - 1 2 %
  - arg_cong 2 %
  - psubr inj_def1 %
  - psub 1 2 %

lemma the1: ∀a. (THE b. a = b) = a
  - sub[λx. (THE y. x y) = a, λx. x = a, λx. a = x] %
  - ext %
  - eq_com_eq %
  - the %

lemma the_inj: ∀f. inj f  ⟶  ∀a. (THE b. f b = f a) = a
  - psub inj_def_eq 1
  - sub[λx. (THE y. x y) = b, λx. x = b, λx. a x = a b] %
  - ext %
  - eq_com 1 %
  - the %

lemma the_inj1: ∀f. inj f  ⟶  ∀a. (THE b. f a = f b) = a
  - sub[λx. (THE y. x y) = b, λx. a x = a b, λx. a b = a x] %
  - ext %
  - eq_com_eq %
  - the_inj 1 %

lemma suc_inj1: inj Suc
  - psubr inj_def1 %
  - Suc_inj 1 %

lemma pred_suc: ∀a. pred (Suc a) = a
  - eq_tran pred_def1 %
  - the_inj1 suc_inj1 %

lemma suc_pred: ∀a. ¬(a = 0)  ⟶  Suc (pred a) = a
  - nat_exh1[a] %
  - falE2 2 1 %
  - exiE[#2.10.b] 2 %
  - subr[#..a] 2 %
  - arg_cong %
  - eq_tran1 pred_suc refl %

lemma neq_0_exi_suc: ∀a. ¬(a = 0) = (∃b. a = Suc b)
  - iffI %
  - nat_exh1[a] %
  - falE2 2 1 %
  - 2 %
  - exiE[#1.10.b] 1 %
  - imp_swap cpos_pn 1 %
  - subr[#..a] 1 nat_dif %

lemma lt_simp3: ∀a b. (Suc a < Suc b) = (a < b)
  - iffI %
  - psub lt_def 1
  - psubr lt_def %
  - exiE[#1.10.c] 1 %
  - conjE1 1+
  - conjE1 2+
  - conjE2 2
  - conjE2 1
  - exiE[λx. c x = Suc b] 3 %
  - exiI[λx. pred (c x)] %
  - conjI %
  - conjI %
  - subr[λx. pred x = Suc a] 1 %
  - eq_tran pred_suc refl %
  - subr[λx. pred x = Suc (pred (c e))] 2+ %
  - eq_tran pred_suc %
  show [∀x. ¬(c x = 0)]
  - suc_pred 4
  - eq_com 4 %
  - nat_exh1[f] %
  - arg_cong[c] 4
  - notI %
  - eq_tran2 5 4
  - eq_tran 4 1
  - falI 3 nat_dif %
  - exiE 4 %
  - notI %
  - arg_cong[c] 4*
  - eq_tran2 5 4
  - eq_tran 4 2
  - falI 3 nat_dif %
  - exiI[d] %
  - subr[λx. pred x = b] 3 %
  - pred_suc %
  - psub lt_def 1
  - psubr lt_def %
  - exiE 1 %
  - conjE1 1+
  - conjE1 2+
  - conjE2 2
  - conjE2 1
  - exiI[λx. Suc (c x)] %
  - conjI %
  - conjI %
  - arg_cong 1 %
  - arg_cong 2 %
  - exiE[#3.10.e] 3 %
  - exiI[d] %
  - arg_cong 3 %

lemma not_lt_refl: ∀a. ¬(a < a)
  - nat_ind[#..a] %
  - lt_simp2 %
  - imp_swap cpos_pp 1 %
  - psub lt_simp3 1 %

lemma lt_suc: ∀a. a < Suc a
  - nat_ind[#..a] %
  - lt_simp1 %
  - psubr lt_simp3 1 %

lemma nat_inf: ∀a. ∃b. a < b
  - exiI[Suc a] %
  - lt_suc %

lemma gt_imp_neq_0: ∀a b. a < b  ⟶  ¬(b = 0)
  - notI %
  - sub[#1..b] 2 1
  - falI 1 lt_simp2 %

def lt_tran_prop: λa. ∀b c. a < b  ⟶  b < c  ⟶  a < c

lemma lt_tran_prop_def1: ∀a. lt_tran_prop a = ∀b c. a < b  ⟶  b < c  ⟶  a < c
  - fun_cong lt_tran_prop_def %

lemma neq_0_imp_gt_0: ∀a. ¬(a = 0)  ⟶  0 < a
  - psub neq_0_exi_suc 1
  - exiE[#1.10.b] 1 %
  - subr[#..a] 1 %
  - lt_simp1 %

lemma lt_tran: ∀a b c. a < b  ⟶  b < c  ⟶  a < c
  show [lt_tran_prop 0, (∀a. lt_tran_prop a  ⟶  lt_tran_prop (Suc a))]
  - nat_ind 3 {1}4
  - psub eta1 3
  - psub lt_tran_prop_def1 3 1 2 %
  - psubr lt_tran_prop_def1 %
  show [¬(e = 0)]
  - neq_0_imp_gt_0 5 %
  - gt_imp_neq_0 4 %
  - psub lt_tran_prop_def1 4
  - psubr lt_tran_prop_def1 %
  - gt_imp_neq_0 5+
  - gt_imp_neq_0 6+
  - psub neq_0_exi_suc 7*
  - psub neq_0_exi_suc 8*
  - exiE[#7.10.i] 7 %
  - exiE[#7.10.j] 7 %
  - sub[#5..e] 7+ 5*
  - sub[#6..e] 7 6*
  - sub[#6..f] 7+ 6*
  - subr[#..f] 7 %
  - psub lt_simp3 5*
  - psub lt_simp3 6*
  - psubr lt_simp3 %
  - 4 5 6 %

lemma gt_0_neq_0: ∀a. (0 < a) = ¬(a = 0)
  - iffI %
  - notI %
  - sub[#1..a] 2 1
  - falI 1 not_lt_refl %
  - neq_0_imp_gt_0 1 %

lemma gt_neq_0_eq: ∀a. (∃b. b < a) = ¬(a = 0)
  - iffI %
  - exiE[#1.10.b] 1 %
  - gt_imp_neq_0 1 %
  - psub neq_0_exi_suc 1
  - exiE[#1.10.b] 1 %
  - subr[#..a] 1 %
  - exiI[0] %
  - lt_simp1 %

lemma gt_neq_0: ∀a b. b < a  ⟶  ¬(a = 0)
  - psub gt_neq_0_eq %
  - exiI[b] %
  - 1 %

lemma neq_suc: ∀a. ¬(a = Suc a)
  - nat_ind[#..a] %
  - nat_dif %
  - imp_swap cpos_pp 1 %
  - Suc_inj 1 %

lemma lt_suc_ab: ∀a b. a = b  ⟶  a < Suc b
  - sub[#..b] 1 %
  - lt_suc %

lemma lt_lt_suc: ∀a b. a < b  ⟶  a < Suc b
  - nat_ind[λa. ∀b. a < b  ⟶  a < Suc b] %
  - lt_simp1 %
  - psubr lt_simp3 %
  - gt_neq_0 3+
  - psub neq_0_exi_suc 4
  - exiE[#4.10.f] 4 %
  - sub[#3..d] 4+ 3*
  - subr[#..d] 4 %
  - psub lt_simp3 3
  - 2 3 %
  - 1 %

lemma gt_exi_suc: ∀a b. a < b  ⟶  ∃c. b = Suc c
  - gt_neq_0 1
  - psub neq_0_exi_suc 1 %

lemma suc_lt_lt: ∀a b. Suc a < b  ⟶  a < b
  - nat_exh1[a] %
  - subr[#..a] 2 %
  - gt_neq_0 1
  - psub neq_0_exi_suc 1
  - exiE 1 %
  - subr[#..b] 1 %
  - lt_simp1 %
  - exiE[#2.10.c] 2 %
  - gt_exi_suc 1+
  - exiE[#3.10.d] 3 %
  - sub[#1..b] 3+ 1*
  - subr[#..b] 3 %
  - psub lt_simp3 1*
  - lt_lt_suc 1 %

lemma lt_exh: ∀a b. (a < b) = (¬(b = 0) ∧ (a = 0 ∨ pred a < pred b))
  - iffI %
  - conjI %
  - gt_neq_0 1 %
  - nat_exh1[a] %
  - disjI1 2 %
  - gt_exi_suc 1+
  - exiE[#2.10.c] 2 %
  - exiE[#2.10.d] 2 %
  - sub[#1..a] 2+ 1+
  - sub[#4..b] 3+ 4
  - psub lt_simp3 4
  show [pred a = c, pred b = d]
  show [pred a < pred b]
  - disjI2 7 %
  - subr[#4..c] 5 4*
  - subr[#4..d] 5 4 %
  - subr[#..a] 2 %
  - pred_suc %
  - subr[#..b] 3 %
  - pred_suc %
  - conjE1 1+
  - conjE2 1
  - psub neq_0_exi_suc 1*
  - exiE[#1.10.c] 1 %
  - sub[#1..b] 2+ 1*
  - subr[#..b] 2 %
  - sub[λx. a = 0 ∨ pred a < x] pred_suc 1
  - disjE 1 %
  - subr[#..a] 1 %
  - lt_simp1 %
  - nat_exh1[a] %
  - subr[#..a] 2 %
  - lt_simp1 %
  - exiE 2 %
  - sub[#1..a] 2+ 1*
  - subr[#..a] 2 %
  - sub[λx. x < c] pred_suc 1
  - psubr lt_simp3 1 %

lemma suc_inj_eq: ∀a b. (Suc a = Suc b) = (a = b)
  - iffI %
  - Suc_inj 1 %
  - arg_cong 1 %

lemma exiE1: ∀P Q. (∃b. Q b)  ⟶  (∀c. Q c  ⟶  P)  ⟶  P
  - exiE[#1.10.c] 1 %
  - 1 2 %

lemma inj_suc: inj Suc
  - suc_inj1 %

lemma pred_eq_0: ∀a. pred a = 0  ⟶  a = 0 ∨ a = Suc 0
  - nat_ind[λa. pred a = 0  ⟶  a = 0 ∨ a = Suc 0] %
  - disjI1 refl %
  - eq_tran2 pred_suc 3
  - arg_cong 3
  - disjI2 3 %
  - 1 %

lemma suc_eq: ∀a b. (Suc a = Suc b) = (a = b)
  - iffI %
  - Suc_inj 1 %
  - arg_cong 1 %

lemma lt_suc_lte: ∀a b. a < b  ⟶  Suc a <= b
  - psubr lte_def %
  - gt_exi_suc 1+
  - exiE[#2.10.c] 2 %
  - sub[#1..b] 2+ 1*
  - subr[#..b] 2 %
  - subr[λx. x ∨ Suc a = Suc c] lt_simp3 %
  - subr[λx. a < c ∨ x] suc_eq %
  - nat_ind[λa. ∀c. a < Suc c  ⟶  a < c ∨ a = c] %
  - nat_exh1[b] %
  - eq_com 3
  - disjI2 3 %
  - exiE 3 %
  show [0 < b]
  - disjI1 4 %
  - subr[#..b] 3 %
  - lt_simp1 %
  - psub lt_simp3 3
  - gt_exi_suc 3+
  - exiE 4 %
  - sub[#3..d] 4+ 3*
  - subr[#..d] 4 %
  - subr[λx. x ∨ Suc b = Suc e] lt_simp3 %
  - subr[λx. b < e ∨ x] suc_eq %
  - 2 3 %
  - 1 %

lemma lt_not_refl: ∀a. ¬(a < a)
  - not_lt_refl %

lemma eq_imp_not_lt: ∀a b. a = b  ⟶  ¬(a < b)
  - sub[#..b] 1 lt_not_refl %

lemma lt_imp_neq: ∀a b. a < b  ⟶  ¬(a = b)
  - cpos_pn eq_imp_not_lt 1 %

lemma lt_imp_not_gt: ∀a b. a < b  ⟶  ¬(b < a)
  - notI %
  - lt_tran 1 2
  - falI 1 lt_not_refl %

lemma gte_0: ∀a. 0 <= a
  - psubr lte_def %
  - nat_exh1[a] %
  - eq_com 1
  - disjI2 1 %
  - exiE[#1.10.b] 1 %
  - subr[#..a] 1 %
  - disjI1 lt_simp1 %

lemma lt_exh_suc: ∀a b. (a < b) = (¬(b = 0) ∧ (a = 0 ∨ Suc a < Suc b))
  - iffI %
  - conjI %
  - gt_neq_0 1 %
  - psubr lt_simp3 1
  - disjI2 1 %
  - conjE1 1+
  - conjE2 1
  - sub[λx. a = 0 ∨ x] lt_simp3 2
  - disjE 2 %
  - psubr lt_exh %
  - conjI %
  - 1 %
  - disjI1 2 %
  - 2 %

lemma nlt_ngt_imp_eq: ∀a b. ¬(a < b)  ⟶  ¬(b < a)  ⟶  a = b
  - nat_ind[λa. ∀b. ¬(a < b)  ⟶  ¬(b < a)  ⟶  a = b] %
  del 1 2 4
  - notE2 %
  - cpos_pp eq_com 2
  - psub neq_0_exi_suc 2
  - exiE 2 %
  - sub[#1..c] 2 1
  - falI lt_simp1 1 %
  del 1 2
  - nat_exh1[d] %
  - sub[#3..d] 4 3
  - falE2 lt_simp1 3 %
  - exiE 4 %
  - sub[#2..d] 4+ 2*
  - psubr lt_simp3
  - cpos_pp 5+ 2*
  - sub[#3..d] 4+ 3*
  - cpos_pp 5 3*
  - 1* 2 3
  - subr[#..d] 2 %
  - arg_cong 1 %
  - 1 %
  - 2 %

lemma disj_imp: ∀P Q. (P ∨ Q) = (¬P  ⟶  Q)
  - iffI %
  - disjE 1 %
  - falE2 2 1 %
  - 2 %
  - split[a] %
  - disjI1 2 %
  - 1 2
  - disjI2 1 %

lemma lt_or_gt_or_eq: ∀a b. a < b ∨ b < a ∨ a = b
  - psubr disj_imp %
  - dmrg_nd 1
  - conjE1 1+
  - conjE2 1
  - nlt_ngt_imp_eq 1 2 %

lemma cpos2_pn: ∀P Q. (P  ⟶  ¬¬Q)  ⟶  (P  ⟶  Q)
  - 1 2
  - notE 1 %

lemma cpos2_np: ∀P Q. (¬¬P  ⟶  Q)  ⟶  (P  ⟶  Q)
  - notI2 2
  - 1 2 %

lemma cpos2_nn: ∀P Q. (¬¬P  ⟶  ¬¬Q)  ⟶  (P  ⟶  Q)
  - notI2 2
  - 1 2
  - notE 1 %

lemma conj_imp_npp: ∀P Q. ¬(P ∧ Q)  ⟶  P  ⟶  ¬ Q
  - notI %
  - conjI 2 3
  - falI 2 1 %

lemma conj_imp_npn: ∀P Q. ¬(P ∧ ¬Q)  ⟶  P  ⟶  Q
  - notE2 %
  - conjI 2 3
  - falI 2 1 %

lemma lt_gt_fal: ∀a b. a < b  ⟶  b < a  ⟶  False
  - lt_imp_not_gt 1*
  - falI 2 1 %

lemma lt_trich: ∀a b. (a < b ∧ ¬(b < a) ∧ ¬(a = b)) ∨ (¬(a < b) ∧ b < a ∧ ¬(a = b)) ∨ (¬(a < b) ∧ ¬(b < a) ∧ a = b)
  - psubr disj_imp %
  - dmrg_nd 1
  - conjE1 1+
  - conjE2 1
  - conj_imp_npn 1*
  - conj_imp_npn 2*
  - conjI %
  - conjI %
  del 2
  - notI %
  - lt_imp_not_gt 2+
  - lt_imp_neq 2+
  - conjI 2* 3
  - 1* 2
  - falI 1 2 %
  del 1
  - notI %
  - lt_imp_not_gt 2+
  - lt_imp_neq 2+
  - conjI 3 2*
  - 1* 2
  - eq_com 1*
  - falI 1 2 %
  - notE2 %
  - cpos_pp 1* 3+
  - conj_imp_npn 1*
  - cpos_pp 2* 3+
  - conj_imp_npp 2*
  - split[a < b] %
  - 1* 4+
  - lt_gt_fal 1 4 %
  - 2* 4
  - cpos_pp 1* 2+
  - nlt_ngt_imp_eq 1 2
  - falI 2 1 %

type pair 2
const Pair :: 'a  ⟹  'b  ⟹  pair 'a 'b

const Pair⁻¹_1 :: pair 'a 'b  ⟹  'a
const Pair⁻¹_2 :: pair 'a 'b  ⟹  'b
axiom Pair_inj1: ∀a b. Pair⁻¹_1 (Pair a b) = a
axiom Pair_inj2: ∀a b. Pair⁻¹_2 (Pair a b) = b

axiom pair_ind: ∀P. (∀a b. P (Pair a b))  ⟶  (∀) P

def fst: THE F. ∀a b. F (Pair a b) = a
def snd: THE F. ∀a b. F (Pair a b) = b

lemma theI: ∀P a. P a  ⟶  (∀b. P b  ⟶  b = a)  ⟶  (THE) P = a
  show [∃!x. a x]
  - uniqE[#3.10.d] 3
  show [a ((THE) a)]
  - 2 4 %
  - imp_swap psub 3 %
  - arg_cong %
  - arg_cong %
  - ext %
  - refl %
  - uniqI[#.10.d] %
  - exiI[b] %
  - 1 %
  - 2+ 3*
  - 2 4
  - eq_tran1 2 3 %

lemma eq_tran': ∀a b c. c = a  ⟶  c = b  ⟶  b = a
  - eq_tran2 1 2
  - eq_com 1 %

lemma tran': ∀a b c. c = a  ⟶  c = b  ⟶  b = a
  - eq_tran' 1 2 %

lemma Pair_inj: ∀a b c d. Pair a b = Pair c d  ⟶  a = c ∧ b = d
  - conjI %
  - arg_cong 1 [Pair⁻¹_1]
  - tran' Pair_inj1 1
  - tran' Pair_inj1 1 %
  - arg_cong 1 [Pair⁻¹_2]
  - tran' Pair_inj2 1
  - tran' Pair_inj2 1 %

lemma fst_simp: ∀a b. fst (Pair a b) = a
  show [∃!F. ∀a b. F (Pair a b) = a]
  - uniqE[#1.10.c] 1
  - subr[#..fst] fst_def %
  - 1 %
  - uniqI %
  - exiI[λp. THE a. ∃b. (λx y. y) (a = b) (p = Pair a b)] %
  - theI %
  - exiI[b] %
  - refl %
  - exiE 1 %
  - Pair_inj 1
  - conjE1 1
  - eq_com 1 %
  - ext %
  - pair_ind[#..c] %
  - eq_tran1 1 %
  - eq_tran 1 refl %

lemma snd_simp: ∀a b. snd (Pair a b) = b
  show [∃!F. ∀a b. F (Pair a b) = b]
  - uniqE[#1.10.c] 1
  - subr[#..snd] snd_def %
  - 1 %
  - uniqI %
  - exiI[λp. THE y. ∃x. (λx y. y) (x = y) (p = Pair x y)] %
  - theI %
  - exiI[a] %
  - refl %
  - exiE 1 %
  - Pair_inj 1
  - conjE2 1
  - eq_com 1 %
  - ext %
  - pair_ind[#..c] %
  - eq_tran1 1 %
  - eq_tran 1 refl %

def if: THE F. ∀a b. F True a b = a ∧ F False a b = b

lemma dmrg_pe1: ∀P. (∃a. ¬P a)  ⟶  ¬(∀a. P a)
  - notI %
  - exiE[#1.10.b] 1 %
  - falI 1 2 %

type unit 0
const Unit :: unit

axiom unit_ind: ∀P. P Unit  ⟶  (∀) P

lemma not_the_imp_p: ¬(∀P a. (THE a. P a) = a  ⟶  P a)
  - dmrg_pe1[#.110.a] %
  - exiI[λx. False] %
  - dmrg_pe1[#.110.a] %
  - exiI[Unit] %
  - notI %
  show [(THE a. False) = Unit]
  - 1 2 %
  - unit_ind[λx. x = Unit] refl %

lemma if_simps: ∀a b. if True a b = a ∧ if False a b = b
  show [∃!F. ∀a b. F True a b = a ∧ F False a b = b]
  - uniqE[#1.10.c] 1
  - subr[#..if] if_def %
  - conjI %
  - conjE1 1 %
  - conjE2 1 %
  - uniqI %
  - exiI[λP a b. THE x. (P  ⟶  x = a) ∧ (¬P  ⟶  x = b)] %
  - conjI %
  - theI %
  - conjI %
  - refl %
  - falE2 true 1 %
  - conjE1 1
  - 1 true %
  - theI %
  - conjI %
  - falE 1 %
  - refl %
  - conjE2 1
  - 1 nfalse %
  - ext %
  - ext %
  - ext %
  - 1*[d, e]
  - 2*[d, e]
  - bool_exh[c] %
  - subr[#..c] 3 %
  - conjE1 1*
  - conjE1 2*
  - eq_tran1 1 2 %
  - subr[#..c] 3 %
  - conjE2 1*
  - conjE2 2*
  - eq_tran1 1 2 %

lemma if_simp1: ∀a b. if True a b = a
  - conjE1 if_simps %

lemma if_simp2: ∀a b. if False a b = b
  - conjE2 if_simps %

def nat_fold: THE F. ∀z f n. F z f 0 = z ∧ F z f (Suc n) = f (F z f n)

lemma uni_eq_fun_true: (∀) = (=) (λx. True)
  - ext %
  - iffI %
  - eta[a]
  - subr[#1..a] 2 1
  - eq_com %
  - ext %
  - eq_truI 1 %
  - sub[#..a] 1 %
  - true %

lemma uniqE2: ∀P a b. (∃!) P  ⟶  P a  ⟶  P b  ⟶  a = b
  show [a = λx. a x]
  sub 4
  - psub uniq_def 1*
  - conjE2 1*
  - 1 2 3 %
  - ext %
  - refl %

lemma uniq2fun: ∀P. (∀a. (∃!) (P a))  ⟶  ∃!f. ∀a b. (f a = b) = (P a b)
  show [(∀b. (∃!) (a b)) = (∀b. ∃!c. a b c)]
  - psub 2 {1}1
  - uniqI[#.10.d] %
  - exiI[λx. THE y. a x y] %
  - 1+*[b]
  - uniqE[#1.10.d] 2*
  - iffI %
  - sub[#..c] 3 2 %
  - uniqE2 1 2 3 %
  - ext %
  - 1*[d]
  - 2*[d]
  - 3*[d]
  - uniqE[#1.10.e] 1*
  - psubr 2* 1+
  - psubr 3* 1
  - eq_tran1 1 2 %
  del 1
  - arg_cong %
  - ext %
  - arg_cong %
  - ext %
  - refl %

lemma lte_refl: ∀a. a <= a
  - psubr lte_def %
  - disjI2 refl %

lemma lte_0_eq_0: ∀a. (a <= 0) = (a = 0)
  - iffI %
  - psub lte_def 1
  - disjE 1 %
  - falE2 1 lt_simp2 %
  - 1 %
  - subr[#..a] 1 lte_refl %

lemma lte_uniq_fun: ∀P. (∀N. ∃!F. ∀n. n <= N  ⟶  P (F n))  ⟶  ∃!F. ∀n. (λx y. y) (n <= n) (P (F n))
  - uniqI[#.10.e] %
  - exiI[λN. (THE F. ∀n. n <= N  ⟶  a (F n)) N] %
  - 1[b]
  - uniqE[#1.10.c] 1 lte_refl %
  - ext %
  - 1*[d]
  - uniqE2[#1.10.e] 1* [b, c]
  show [∀e. e <= d  ⟶  a (b e), ∀f. f <= d  ⟶  a (c f)]
  - 1* {1}4 {1}5
  - fun_cong 1 %
  - 2 %
  - 3 %

lemma lt_imp_lte: ∀a b. a < b  ⟶  a <= b
  - psubr lte_def %
  - disjI1 1 %

lemma eq_imp_lte: ∀a b. a = b  ⟶  a <= b
  - sub[#..b] 1 lte_refl %

lemma lte_suc2: ∀a b. (Suc a <= Suc b) = (a <= b)
  - iffI %
  - psub lte_def 1
  - disjE 1 %
  - psub lt_simp3 1
  - lt_imp_lte 1 %
  - Suc_inj 1
  - eq_imp_lte 1 %
  - psub lte_def 1
  - disjE 1 %
  - psubr lt_simp3 1
  - lt_imp_lte 1 %
  - arg_cong 1 [Suc]
  - eq_imp_lte 1 %

lemma lt_suc_lte1: ∀a b. a < Suc b  ⟶  a <= b
  - lt_suc_lte 1
  - psub lte_suc2 1 %

lemma nat_ind_lte: ∀P. P 0  ⟶  (∀N. (∀n. n <= N  ⟶  P n)  ⟶  P (Suc N))  ⟶  ∀n. P n
  show [∀N n. n <= N  ⟶  a n]
  - 3 lte_refl %
  - nat_ind[λN. ∀n. n <= N  ⟶  a n] [d, d] %
  del 3
  - psub lte_0_eq_0 3
  - subr 3 1 %
  del 3
  - 2+ {1}3+
  - psub lte_def 4*
  - disjE 4 %
  - lt_suc_lte1 5
  - 3 5 %
  - subr 5 4 %
  - lte_refl %

lemma not_suc_lt: ∀a. ¬(Suc a < a)
  - notI %
  - lt_lt_suc 1
  - falI 1 lt_not_refl %

lemma not_suc_lte: ∀a. ¬(Suc a <= a)
  - notI %
  - psub lte_def 1
  - disjE 1 %
  - falI 1 not_suc_lt %
  - eq_com 1
  - falI 1 neq_suc %

lemma not_lte_exi_ind: ¬(∀P. (∀N. ∃n. n <= N  ⟶  P n)  ⟶  ∀n. P n)
  - dmrg_pe1[#.110.a] %
  - exiI[λx. False] %
  - notI %
  - 1 %
  - exiI[Suc a] %
  - falI 1 not_suc_lte %

lemma quant_eq1: ∀P Q R. (∀a. P a  ⟶  Q a)  ⟶  (∀a. Q a  ⟶  P a)  ⟶  R P = R Q
  - iffI 1 2
  - ext {1}1
  - arg_cong 1 %

lemma quant_eq: ∀P Q R. R P  ⟶  (∀a. P a  ⟶  Q a)  ⟶  (∀a. Q a  ⟶  P a)  ⟶  R Q
  - quant_eq1 {1}2 {1}3 [c]
  - psub 2 1 %

lemma suc_lte_lt: ∀a b. Suc a <= b  ⟶  a < b
  - psub lte_def 1
  - disjE 1 %
  - suc_lt_lt 1 %
  - eq_com 1
  sub 1
  - lt_suc %

lemma lt_neq_pred_lt_suc: ∀a b. a < b  ⟶  ¬(b = Suc a)  ⟶  a < Suc b
  - lt_suc_lte 1*
  - suc_lte_lt 1*
  - lt_lt_suc 1 %

lemma disj_not: ∀P Q. P ∨ Q  ⟶  P ∨ (¬P ∧ Q)
  - disjE 1 %
  - disjI1 1 %
  - split[a] %
  - disjI1 2 %
  - conjI 2 1
  - disjI2 1 %

lemma sub1: ∀P a b. P a  ⟶  a = b  ⟶  P b
  - sub 2 1 %

lemma theE: ∀P a. a = (THE) P  ⟶  (∃!) P  ⟶  P a
  - psub eta1 2
  - uniqE 2
  sub 1
  - sub1 1 %
  - arg_cong %
  - ext %
  - refl %
lemma lte_suc: ∀a. a <= Suc a
  - lt_imp_lte %
  - lt_suc %

lemma if_tru: ∀P Q a b. P (if Q a b)  ⟶  Q  ⟶  P a
  - eq_truI 2
  sub 2
  - sub1 1 %
  - if_simp1 %

lemma if_fal: ∀P Q a b. P (if Q a b)  ⟶  ¬Q  ⟶  P b
  - eq_falI 2
  sub 2
  - sub1 1 %
  - if_simp2 %

lemma if_tru1: ∀P a b. if P a b  ⟶  P  ⟶  a
  - if_tru[λx. x] 1 2 %

lemma if_fal1: ∀P a b. if P a b  ⟶  ¬P  ⟶  b
  - if_fal[λx. x] 1 2 %

lemma lte_lte_suc: ∀a b. a <= b  ⟶  a <= Suc b
  - psub lte_def 1
  - disjE 1 %
  - lt_lt_suc 1
  - lt_imp_lte 1 %
  sub 1
  - lte_suc %

lemma lte_suc_suc: ∀a. a <= Suc (Suc a)
  - lte_lte_suc %
  - lte_suc %

lemma suc_lte_neq_0: ∀a b. Suc a <= b  ⟶  ¬(b = 0)
  - psub lte_def 1
  - disjE 1 %
  - gt_neq_0 1 %
  - eq_com 1
  - notI %
  sub 2
  - falI 1 nat_dif %

lemma if_tru_r: ∀P Q R. P  ⟶  Q  ⟶  if P Q R
  - eq_truI 1*
  sub 1
  - psubr if_simp1 1 %

lemma if_fal_r: ∀P Q R. ¬P  ⟶  R  ⟶  if P Q R
  - eq_falI 1*
  sub 1
  - psubr if_simp2 1 %

lemma if_tru_t: ∀P a b. P  ⟶  if P a b = a
  - eq_truI 1
  sub 1
  - if_simp1 %

lemma if_fal_t: ∀P a b. ¬P  ⟶  if P a b = b
  - eq_falI 1
  sub 1
  - if_simp2 %

lemma not_suc_lte_0: ∀a. ¬(Suc a <= 0)
  - notI %
  - psub lte_0_eq_0 1
  - eq_com 1
  - falI 1 nat_dif %

lemma suc_neq_0: ∀a. ¬(Suc a = 0)
  - notI %
  - eq_com 1
  - falI 1 nat_dif %

lemma not_all_exi_dif: ¬(∀a. ∃b. ¬(b = a))
  - notI %
  - 1[Unit]
  - dmrg_pe1[λx. x = Unit] 1
  - imp_swap cpos_np 1 %
  del 1
  - unit_ind[#..a] refl %

def (∈) [infixl 52]: λx S. (λx y. y) (S = λx. True) S x

lemma in_def: ∀S a. (a ∈ S) = (S a)
  - ∈_def
  - fun_cong2 1 %

def ∅: λa. False

lemma emp_def: ∅ = λa. False
  - ∅_def %

lemma emp_def1: ∀a. ∅ a = False
  - subr[#..∅] emp_def refl %

lemma not_in_emp: ∀a. ¬(a ∈ ∅)
  - notI %
  - psub in_def 1
  - psub emp_def1 1 %

def univ: λa. True

lemma univ_def1: ∀a. univ a = True
  - subr[#..univ] univ_def refl %

lemma emp_neq_univ: ¬(∅ = univ)
  - notI %
  - fun_cong 1 [undefined]
  - eq_tran2 emp_def1 1
  - eq_com 1
  - eq_tran2 univ_def1 1
  - bool_dif 1 %

lemma all_in_univ: ∀a. a ∈ univ
  - psubr in_def %
  - psubr univ_def1 true %

lemma emp_in_univ: ∅ ∈ univ
  - all_in_univ %

lemma not_univ_in_emp: ¬(univ ∈ ∅)
  - not_in_emp %

lemma nemp_exi_in: ∀S. ¬(S = ∅) = (∃a. a ∈ S)
  - iffI %
  - imp_swap cpos_np 1 %
  - dmrg_ne 1
  - imp_swap eq_tran1 emp_def %
  - ext %
  - 1[b]
  - eq_falI %
  - imp_swap cpos_pp 1 %
  - psubr in_def 1 %
  - notI %
  sub 2
  - exiE 1 %
  - falI 1 not_in_emp %

lemma cposr_pp: ∀P Q. P  ⟶  (¬Q  ⟶  ¬P)  ⟶  Q
  - cpos_nn 2 1 %

lemma cposr_pn: ∀P Q. P  ⟶  (Q  ⟶  ¬P)  ⟶  ¬Q
  - cpos_pn 2 1 %

lemma cposr_np: ∀P Q. ¬P  ⟶  (¬Q  ⟶  P)  ⟶  Q
  - cpos_np 2 1 %

lemma cposr_nn: ∀P Q. ¬P  ⟶  (Q  ⟶  P)  ⟶  ¬Q
  - cpos_pp 2 1 %

lemma if_tru_t1: ∀P a b c. if P a b = c  ⟶  P  ⟶  a = c
  - eq_truI 2
  sub 2
  - eq_tran2 if_simp1 1 %

lemma if_fal_t1: ∀P a b c. if P a b = c  ⟶  ¬P  ⟶  b = c
  - eq_falI 2
  sub 2
  - eq_tran2 if_simp2 1 %

lemma if_tru_t2: ∀P a b c. if P a b = c  ⟶  P  ⟶  c = a
  - if_tru_t1 1 2
  - eq_com 1 %

lemma if_fal_t2: ∀P a b c. if P a b = c  ⟶  ¬P  ⟶  c = b
  - if_fal_t1 1 2
  - eq_com 1 %

lemma if_tru_r1: ∀P a b c. P  ⟶  a = c  ⟶  if P a b = c
  sub 2
  - if_tru_t 1 %

lemma if_fal_r1: ∀P a b c. ¬P  ⟶  b = c  ⟶  if P a b = c
  sub 2
  - if_fal_t 1 %

lemma if_tru_r2: ∀P a b c. P  ⟶  c = a  ⟶  if P a b = c
  - eq_com  2
  - if_tru_r1 1 2 %

lemma if_fal_r2: ∀P a b c. ¬P  ⟶  c = b  ⟶  if P a b = c
  - eq_com 2
  - if_fal_r1 1 2 %

lemma if_args_eq: ∀P a. if P a a = a
  - split[a] %
  - if_tru_t 1 %
  - if_fal_t 1 %

lemma if_eq_if: ∀P a b c d. (P  ⟶  a = c)  ⟶  (¬P  ⟶  b = d)  ⟶  if P a b = if P c d
  - split[a] %
  del 2
  - 1* 2+
  - if_tru_r2 2+ %
  - if_tru_r2 2 1 %
  del 1
  - 1* 2+
  - if_fal_r2 2+ %
  - if_fal_r2 2 1 %

lemma if_eq: ∀P a b c. (P  ⟶  a = c)  ⟶  (¬P  ⟶  b = c)  ⟶  if P a b = c
  - split[a] %
  del 2
  - 1* 2+
  - if_tru_r1 2 1 %
  del 1
  - 1* 2+
  - if_fal_r1 2 1 %

lemma ext1: ∀P f. P (λx. f x) = P f
  - arg_cong %
  - ext %
  - refl %

lemma uniq_def1: ∀P. (∃!) P = ((∃) P ∧ (∀ a b. P a  ⟶  P b  ⟶  a = b))
  - sub[#..a] eta uniq_def %

lemma if_tru_eq: ∀P a b c. if P a b = c  ⟶  P  ⟶  a = c
  - if_tru[λx. x = d] 1 2 %

lemma if_fal_eq: ∀P a b c. if P a b = c  ⟶  ¬P  ⟶  b = c
  - if_fal[λx. x = d] 1 2 %

lemma if_tru_eq1: ∀P a b c. if P a b = c  ⟶  P  ⟶  c = a
  - if_tru_eq 1 2
  - eq_com 1 %

lemma if_fal_eq1: ∀P a b c. if P a b = c  ⟶  ¬P  ⟶  c = b
  - if_fal_eq 1 2
  - eq_com 1 %

lemma eq_tran3: ∀a b c d. a = b  ⟶  c = d  ⟶  b = d  ⟶  a = c
  sub 1
  sub 2
  - eq_com 1 %

lemma disjE1: ∀P Q. P ∨ Q  ⟶  ¬P  ⟶  Q
  - disjE 1 %
  - falE2 2 1 %
  - 2 %

lemma disjE2: ∀P Q. P ∨ Q  ⟶  ¬Q  ⟶  P
  - disjE 1 %
  - 2 %
  - falE2 2 1 %

lemma neq0: ∀P a. ¬(a = 0)  ⟶  (∀b. a = Suc b  ⟶  P)  ⟶  P
  - psub neq_0_exi_suc 1*
  - exiE 1* %
  sub 1
  - 1 refl %

lemma cmp: ∀a b P. (a < b  ⟶  P)  ⟶  (b < a  ⟶  P)  ⟶  (a = b  ⟶  P)  ⟶  P
  - lt_or_gt_or_eq [a, b]
  - disjE 4 %
  - disjE 4 %
  - 1 4 %
  - 2 4 %
  - 3 4 %

lemma uniqI1': ∀a P. P a  ⟶  (∀b. P b = (b = a))  ⟶  (∃!) P
  - uniqI %
  - exiI 1 %
  - psub 2+ 3*
  - psub 2+ 4*
  - eq_tran1 3 4 %

lemma uniqI1: ∀a P. P a  ⟶  (∀b. P a  ⟶  P b = (b = a))  ⟶  (∃!) P
  - 2* 1+
  - uniqI1' 1 {1}2 %

lemma gte_suc_neq_0: ∀a b. Suc a <= b  ⟶  ¬(b = 0)
  - notI %
  sub 2
  - falI 1 not_suc_lte_0 %

lemma suc_not_lte_0: ∀a. ¬(Suc a <= 0)
  - not_suc_lte_0 %

lemma neq_com: ∀a b. ¬(a = b)  ⟶  ¬(b = a)
  - cposr_nn 1 %
  - eq_com 1 %

lemma lt_imp_neq1: ∀a b. a < b  ⟶  ¬(b = a)
  - lt_imp_neq 1
  - neq_com 1 %

lemma lt_imp_not_gte: ∀a b. a < b  ⟶  ¬(b <= a)
  - notI %
  - psub lte_def 2
  - disjE 2 %
  - lt_gt_fal 1 2 %
  sub 2
  - falI 1 not_lt_refl %

lemma nat_fold_simps: ∀z f n. nat_fold z f 0 = z ∧ nat_fold z f (Suc n) = f (nat_fold z f n)
  let C: λF. ∀z f n. F z f 0 = z ∧ F z f (Suc n) = f (F z f n)
  - sub[λP. P nat_fold] 1+ %
  - subr nat_fold_def %
  - sub[λF. C ((THE) F)] 1+ %
  - uniqE %
  let K: λF z f n. if (n = 0) z (f (F z f (pred n)))
  let P: λF. ∀z f n. F z f n = K F z f n
  show [C = P]
  sub 4
  del 1
  let P': λN F. ∀z f n. F z f n = if (n <= N) (K F z f n) undefined
  -
  let FF: λN. (THE) (P' N)
  show [∀N. (∃!) (P' N)]
  show [∀N. P' N (FF N)]
  show[∀N z f n. n <= N  ⟶  FF N z f n = FF n z f n]
  -
  - psub uniq_def1 5+
  - conjE1 8+
  - conjE2 8
  -
  - uniqI1[λz f n. FF n z f n] %
  -
  sub 2
  ren a z
  ren b f
  ren c N
  -
  sub 1
  - nat_ind[#..N] %
  - eq_com %
  - if_tru_r2 refl %
  - 4+[0]
  sub 1
  - eq_tran1 7 %
  - eq_com %
  - if_tru_r1 lte_refl %
  - if_tru_r1 refl refl %
  ren a N
  - subr[λx. FF (Suc N) z f (Suc N) = if (Suc N = 0) z (f (FF x z f x))] pred_suc %
  - eq_com %
  - if_fal_r2 suc_neq_0 %
  show [∀N z f. FF (Suc N) z f N = FF N z f N]
  - 9[N, z, f]
  - 4+[Suc N]
  sub 1
  - 9[z, f, Suc N]
  - eq_tran 9 %
  - if_tru_r1 lte_refl %
  - if_fal_r1 suc_neq_0 %
  - arg_cong %
  - subr[λx. FF (Suc N) z f x = FF N z f N] pred_suc 8 %
  del 8
  ren a N
  ren b z
  ren c f
  - 5 lte_suc %
  -
  let F₀: λz f n. FF n z f n
  - subr 11+ 10
  ren a F₁
  - iffI %
  -
  - ext %
  - ext %
  - ext %
  ren a z
  ren b f
  ren c N
  -
  - nat_ind[λn. ∀N z f. n <= N  ⟶  F₁ z f n = FF N z f n] %
  del 11
  sub 2
  - eq_tran 10+ %
  - eq_com %
  sub 2
  - eq_tran 4+ %
  sub 1
  - if_tru_r1 gte_0 %
  - if_tru_r2 refl %
  - if_tru_r1 refl refl %
  -
  ren a n
  ren b N
  ren c z
  ren d f
  sub 2
  - eq_tran 11+ %
  sub 1
  - if_fal_r2 suc_neq_0 %
  sub 1
  - eq_tran 3+ %
  - if_tru_r1 11+ %
  - if_fal_r2 suc_neq_0 %
  - arg_cong %
  - subr[λx. F₁ z f x = FF N z f x] pred_suc %
  - lte_lte_suc 11
  - psub lte_suc2 11
  - 10 11 %
  - lte_refl %
  -
  sub 12
  sub 2
  ren a z
  ren b f
  ren c N
  sub 2
  - eq_tran 4+ %
  - if_tru_r1 lte_refl %
  sub 1
  - if_eq_if %
  - refl %
  - neq0 9 %
  sub 9
  ren a N
  - arg_cong %
  - subr[λx. FF (Suc N) z f x = FF x z f x] pred_suc %
  - 4 lte_suc %
  -
  ren a N
  ren b z
  ren c f
  ren d n
  - nat_ind[λn. ∀N z f. n <= N  ⟶  FF N z f n = FF n z f n] %
  del 7
  del 7
  ren a N
  ren b z
  ren c f
  sub 3
  - eq_tran 5+ %
  - if_tru_r1 gte_0 %
  sub 1
  - if_tru_r2 refl %
  - eq_tran 4+ %
  - if_tru_r1 lte_refl %
  - if_tru_r1 refl refl %
  del 7
  ren a n
  ren b N
  ren c z
  ren d f
  sub 3
  - eq_tran 5+ %
  - if_tru_r1 7+ %
  sub 1
  - if_fal_r2 suc_neq_0 %
  - eq_tran 4+ %
  - if_tru_r1 lte_refl %
  - if_fal_r1 suc_neq_0 %
  - arg_cong %
  - subr[λx. FF (Suc n) z f x = FF N z f x] pred_suc %
  - suc_lte_neq_0 6+
  - psub neq_0_exi_suc 7
  - exiE 7 %
  sub 7
  ren a N
  - psub lte_suc2 6
  - lte_lte_suc 6
  - 5+ lte_suc [z, f]
  - 5+ 6 [z, f]
  - eq_tran1 6 7 %
  - 7 %
  -
  ren a N
  - 5[N]
  - fun_cong 4* [N]
  - theE 4 5 %
  -
  ren a N
  - nat_ind[#..N] %
  -
  - uniqI1[λz f n. if (n = 0) z undefined] %
  sub 3
  ren a z
  ren b f
  ren c n
  - split[n = 0] %
  sub 4
  - if_tru_r2 refl %
  - if_tru_r1 lte_refl %
  sub 1
  - if_tru_r1 refl  refl %
  - neq0 4 %
  sub 4
  ren a n
  - if_fal_r2 suc_neq_0 %
  - if_fal_r1 suc_not_lte_0 refl %
  -
  ren a F
  - iffI %
  - ext %
  - ext %
  - ext %
  ren a z
  ren b f
  ren c N
  sub 3
  - eq_tran 5+ %
  - 4+[z, f, N]
  - imp_swap eq_tran1 6 %
  - if_eq_if %
  - psub lte_0_eq_0 6
  sub 6
  sub 1
  - if_eq_if %
  - refl %
  - falE2 refl 5 %
  - refl %
  sub 6
  - 5 %
  -
  ren a N
  let F₀: (THE) (P' N)
  - theE 6+ 5+
  let F₁: λz f n. if (n = Suc N) (f (F₀ z f N)) (F₀ z f n)
  -
  - uniqI1[F₁] %
  -
  sub 3
  ren a z
  ren b f
  ren c n
  sub 7
  -
  - cmp[n, Suc N] %
  - lt_imp_neq 7+
  - if_fal_r2 8+ %
  - lt_imp_lte 7+
  - if_tru_r2 9+ %
  sub 1
  - eq_tran 5+ %
  - lt_suc_lte 6+
  - psub lte_suc2 9+
  - if_tru_r1 10+ %
  - if_eq_if %
  - refl %
  - arg_cong %
  - neq0 11 %
  sub 11
  ren a n
  - eq_com %
  - if_fal_r2 %
  - subr[λx. ¬(x = Suc N)] pred_suc %
  - suc_lt_lt 6+
  - lt_imp_neq 11 %
  - refl %
  - lt_imp_neq1 7+
  - if_fal_r2 8+ %
  - if_fal_r2 %
  - cposr_nn 8 %
  - psub lte_def 8
  - lt_imp_not_gt 7*
  - disjE1 8 7 %
  - eq_tran 6+ %
  - suc_lt_lt 7+
  - lt_imp_not_gte 9+
  - if_fal_r1 10 refl %
  sub 7
  - if_tru_r2 refl %
  - if_tru_r1 lte_refl %
  sub 1
  - if_fal_r1 suc_neq_0 %
  - arg_cong %
  - if_fal_r2 %
  - subr[λx. ¬(x = Suc N)] pred_suc %
  - neq_suc %
  - subr[λx. F₀ z f N = F₀ z f x] pred_suc refl %
  -
  ren a F₂
  - iffI %
  -
  - ext %
  - ext %
  - ext %
  ren a z
  ren b f
  ren c n
  -
  - nat_ind[#..n] %
  -
  sub 3
  - eq_tran 9+ %
  - if_tru_r2 gte_0 %
  - eq_tran 8+ %
  - if_tru_r2 gte_0 %
  sub 1
  - if_eq_if %
  - refl %
  - falE2 refl 9 %
  -
  ren a n
  sub 3
  - eq_tran 9+ %
  - eq_com %
  - eq_tran 8+ %
  - if_eq_if %
  sub 1
  - if_eq_if %
  - refl %
  del 11
  - arg_cong %
  - eq_com %
  - subr[λx. F₂ z f x = F₁ z f x] pred_suc %
  - 9 %
  - refl %
  sub 10
  - 9 %
  -
  - ext %
  ren a F
  sub 1
  sub 2
  - iffI %
  -
  ren a z
  ren b f
  ren c n
  - split[n = 0] %
  sub 3
  - conjE1 2
  - eq_tran 2 %
  - eq_com %
  sub 1
  - if_tru_r1 refl refl %
  - neq0 3 %
  sub 3
  ren a n
  - conjE2 2
  - eq_tran 2 %
  - eq_com %
  sub 1
  - if_fal_r1 suc_neq_0 %
  - arg_cong %
  - subr[λx. F z f x = F z f n] pred_suc  refl %
  -
  ren a z
  ren b f
  ren c n
  - conjI %
  - eq_tran 2 %
  sub 1
  - if_tru_r1 refl refl %
  - eq_tran 2 %
  sub 1
  - if_fal_r1 suc_neq_0 %
  - arg_cong %
  - subr[λx. F z f x = F z f n] pred_suc refl %

lemma nat_fold_simp1: ∀z f. nat_fold z f 0 = z
  - conjE1 nat_fold_simps %

lemma nat_fold_simp2: ∀z f n. nat_fold z f (Suc n) = f (nat_fold z f n)
  - conjE2 nat_fold_simps %

lemma com: ∀a b. a = b  ⟶  b = a
  - eq_com 1 %

lemma tran: ∀a b c. a = b  ⟶  a = c  ⟶  b = c
  - eq_tran2 1 2 %

lemma tran1: ∀a b c. a = b  ⟶  a = c  ⟶  c = b
  - tran 1 2
  - com 1 %

lemma tranr: ∀a b c. a = b  ⟶  b = c  ⟶  a = c
  - eq_tran 1 2 %

lemma tranr1: ∀a b c. a = b  ⟶  c = b  ⟶  a = c
  - com 2
  - tranr 1 2 %

def (+) [infixl 55]: λa b. nat_fold a Suc b

lemma add_def: ∀a b. a + b = nat_fold a Suc b
  - fun_cong2 +_def %

lemma add_simp1: ∀a b. a + 0 = a
  - tranr add_def %
  - tranr nat_fold_simp1 refl %

lemma add_simp2: ∀a b. a + Suc b = Suc (a + b)
  - tranr add_def %
  - tranr nat_fold_simp2 %
  - arg_cong %
  - com %
  - tranr add_def refl %

lemma add0: ∀a. a + 0 = a
  - add_simp1 %

lemma add0r: ∀a. 0 + a = a
  - nat_ind[#..a] %
  - add0 %
  ren b a
  - tranr add_simp2 %
  - arg_cong 1 %

lemma suc_add: ∀a b. Suc a + b = Suc (a + b)
  - nat_ind[λb. ∀a. Suc a + b = Suc (a + b)] %
  - tranr1 add0 %
  - arg_cong %
  - add0 %
  ren c a
  ren d b
  - tranr1 add_simp2 %
  - arg_cong %
  - tranr1 add_simp2 %
  - 1 %

lemma add_com: ∀a b. a + b = b + a
  - nat_ind[λa. ∀b. a + b = b + a] %
  - tranr1 add0r %
  - add0 %
  ren c a
  ren d b
  - com %
  - tranr1 add_simp2 %
  - tranr suc_add %
  - arg_cong 1 %

lemma injI: ∀f. (∀a b. f a = f b  ⟶  a = b)  ⟶  inj f
  - psubr inj_def1 {2}1 %

lemma injE: ∀f a b. inj f  ⟶  f a = f b  ⟶  a = b
  - psub inj_def1 1 2 %

lemma add_inj1: ∀a b c. a + b = a + c  ⟶  b = c
  - nat_ind[λa. ∀b c. a + b = a + c  ⟶  b = c, a, b, c] %
  del 1
  - tran1 add0r 1
  - tran1 add0r 1 %
  del 1
  ren d a
  ren e b
  ren f c
  - tran1 suc_add 2
  - tran1 suc_add 2
  - Suc_inj 2
  - 1 2 %
  - 1 %

lemma add_inj: ∀a. inj ((+) a)
  - injI {2}add_inj1 %

lemma add_assoc: ∀a b c. (a + b) + c = a + (b + c)
  - nat_ind[λc. ∀a b. a + b + c = a + (b + c)] %
  ren d a
  ren e b
  - tranr add0 %
  - arg_cong %
  - com add0 %
  ren d a
  ren e b
  ren f c
  - tranr1 add_simp2 %
  - subr[λx. b + x = Suc (b + c + a)] add_simp2 %
  - tranr1 add_simp2 %
  - arg_cong 1 %

lemma lte_add: ∀a b. a <= a + b
  - nat_ind[λb. ∀a. a <= a + b] %
  - subr add0 lte_refl %
  - subr add_simp2 %
  - lte_lte_suc 1 %

lemma uniqE1: ∀P Q. (∃!) P  ⟶  (∀a. P a  ⟶  (∀b. P b = (b = a))  ⟶  Q)  ⟶  Q
  - psub uniq_def1 1*
  - conjE1 1+
  - conjE2 1
  - exiE 2* %
  - 1+ 2+ %
  - iffI %
  - 3 4 2 %
  sub 4
  - 2 %

lemma lte_uniq_add: ∀a b. (a <= b) = (∃!c. b = a + c)
  - iffI %
  - nat_ind[λa. ∀b. a <= b  ⟶  ∃!c. b = a + c] %
  del 1
  del 1
  ren c a
  - uniqI1[a] %
  - com add0r %
  sub 1
  - iffI %
  - com 1
  - tran add0r 1 %
  sub 1
  - arg_cong %
  - com add0r %
  del 1
  ren c a
  ren d b
  - gte_suc_neq_0 2+
  - neq0 3 %
  sub 3
  ren c b
  - psub lte_suc2 2
  - 1 2
  - uniqE 1+
  - uniqI1[THE c. b = a + c] %
  - com %
  - tranr suc_add %
  - arg_cong %
  - com 2 %
  - iffI %
  - com 4
  - tran suc_add 4
  - Suc_inj 4
  - com 4
  sub 4
  - uniqE 1+
  - add_inj1 4 %
  - com %
  - tranr suc_add %
  - arg_cong %
  sub 4
  - com %
  - uniqE 1 %
  - 1 %
  - uniqE1 1 %
  sub 1
  ren c b
  - nat_ind[λb. (∀c. (a + b = a + c) = (c = b))  ⟶  a <= a + b] %
  del 1
  - subr add0 lte_refl %
  del 1
  ren c b
  - subr add_simp2 %
  - lte_lte_suc lte_add %
  - 1 %

type list 1

const Nil  :: list 'a
const Cons :: 'a  ⟹  list 'a  ⟹  list 'a

axiom list_dif: ∀a b. ¬(Nil = Cons a b)
axiom Cons_inj: ∀a b c d. Cons a b = Cons c d  ⟶  a = c ∧ b = d
axiom list_ind: ∀P. P Nil  ⟶  (∀a b. P b  ⟶  P (Cons a b))  ⟶  (∀) P

def nul: λa. a = Nil
def nnul: λa. ¬(nul a)

lemma nul_def1: ∀a. nul a = (a = Nil)
  - fun_cong nul_def %

lemma nnul_def1': ∀a. nnul a = ¬(nul a)
  - fun_cong nnul_def %

lemma nnul_def1: ∀a. nnul a = ¬(a = Nil)
  - iffI %
  - fun_cong nnul_def
  - psub 2 1
  - cposr_nn 1 %
  sub 1
  - psubr nul_def1 refl %
  - fun_cong nnul_def
  - psubr 2 %
  - subr nul_def1 1 %

lemma nul_simp1: nul Nil = True
  - eq_truI %
  - psubr nul_def1 refl %

lemma nul_simp2: ∀a b. nul (Cons a b) = False
  - eq_falI %
  - notI %
  - psub nul_def1 1
  - com 1
  - falI 1 list_dif %

lemma nnul_simp1: nnul Nil = False
  - eq_falI %
  - subr nnul_def1 %
  - notI2 refl %

lemma nnul_simp2: ∀a b. nnul (Cons a b) = True
  - eq_truI %
  - psubr nnul_def1 %
  - neq_com list_dif %

lemma nnul_exi_cons: ∀a. nnul a = (∃b c. a = Cons b c)
  - list_ind[#..a] %
  - tranr1 nnul_simp1 %
  - eq_falI %
  - notI %
  - exiE 1 %
  - exiE 1 %
  - falI 1 list_dif %
  - tranr1 nnul_simp2 %
  - eq_truI %
  - exiI[b] %
  - exiI[c] %
  - refl %

lemma nnul_imp_uniq_cons: ∀a. nnul a = (∃!b c. a = Cons b c)
  - iffI %
  - psub nnul_exi_cons 1
  - exiE 1 %
  - exiE 1 %
  sub 1
  - uniqI1[b] %
  - uniqI1[c] %
  - refl %
  - iffI %
  - eq_tran2 1 2
  - Cons_inj 1
  - conjE2 1
  - com 1 %
  sub 2
  - 1 %
  - iffI %
  - uniqE 1*
  - uniqE 2*
  - eq_tran2 1 2
  - Cons_inj 1
  - conjE1 1
  - com 1 %
  sub 2
  - uniqI1[c] %
  - refl %
  del 2
  - iffI %
  - Cons_inj 2
  - conjE2 2
  - com 2 %
  sub 2
  - refl %
  - uniqE 1
  - uniqE 1
  sub 1
  - psubr nnul_simp2 true %

lemma nul_simp1p: nul Nil
  - eq_truE %
  - nul_simp1 %

lemma nul_simp2p: ∀a b. ¬(nul (Cons a b))
  - eq_falE %
  - nul_simp2 %

lemma nnul_simp1p: ¬(nnul Nil)
  - eq_falE %
  - nnul_simp1 %

lemma nnul_simp2p: ∀a b. nnul (Cons a b)
  - eq_truE %
  - nnul_simp2 %

def head: λa. if (nnul a) (THE b. ∃c. a = Cons b c) undefined
def tail: λa. if (nnul a) (THE c. ∃b. a = Cons b c) undefined

lemma head_def1: ∀a. head a = if (nnul a) (THE b. ∃c. a = Cons b c) undefined
  - fun_cong head_def %

lemma tail_def1: ∀a. tail a = if (nnul a) (THE c. ∃b. a = Cons b c) undefined
  - fun_cong tail_def %

lemma head_simp: ∀a b. head (Cons a b) = a
  - tranr head_def1 %
  - if_tru_r1 nnul_simp2p %
  - theI %
  - exiI[b] %
  - refl %
  - exiE 1 %
  - Cons_inj 1
  - conjE1 1
  - com 1 %

lemma tail_simp: ∀a b. tail (Cons a b) = b
  - tranr tail_def1 %
  - if_tru_r1 nnul_simp2p %
  - theI %
  - exiI[a] %
  - refl %
  - exiE 1 %
  - Cons_inj 1
  - conjE2 1
  - com 1 %

def inc: Suc

lemma inc_simp: ∀a. inc a = Suc a
  - fun_cong inc_def %

def dec: λa. THE b. a = Suc b

lemma dec_simp: ∀a. dec (Suc a) = a
  - fun_cong dec_def
  - tranr 1 %
  - theI %
  - refl %
  - Suc_inj 1
  - com 1 %

def sub: λa b. THE c. a = b + c

lemma sub_simps: ∀a b. sub a 0 = a ∧ sub (Suc a) (Suc b) = sub a b
  - fun_cong2 sub_def
  - psub lte_uniq_add
  - theE 1+
  - subr[#..sub] sub_def %
  - conjI %
  - 2+[0, a] gte_0
  - uniqE 4
  - com 4
  - tran add0r 4 %
  - arg_cong %
  - ext %
  - iffI %
  - com 4
  - tran suc_add 4
  - Suc_inj 4
  - com 4 %
  sub 4
  - com %
  - tranr suc_add refl %

lemma sub_simp1: ∀a. sub a 0 = a
  - conjE1 sub_simps %

lemma sub_simp2: ∀a b. sub (Suc a) (Suc b) = sub a b
  - conjE2 sub_simps %

def μ [binder]: λP. THE n. P n ∧ (∀k. k < n  ⟶  ¬P k)

lemma mu_def: ∀P. (μ) P = (THE n. P n ∧ (∀k. k < n  ⟶  ¬P k))
  - fun_cong μ_def %

lemma muI: ∀P n. P n  ⟶  (∀k. k < n  ⟶  ¬P k)  ⟶  (μ) P = n
  - tranr mu_def %
  - theI %
  - conjI %
  - 1 %
  - 2 3 %
  - conjE1 3+
  - conjE2 3
  - cmp[c, b] %
  - 2 5
  - falE2 2 4 %
  - 4 5
  - falE2 1 4 %
  - 5 %

lemma muE1: ∀Q P n. Q ((μ) P)  ⟶  P n  ⟶  (∀k. k < n  ⟶  ¬P k)  ⟶  Q n
  - imp_swap psubr 1 %
  - arg_cong %
  - com %
  - muI 1 {1}2 %

lemma not_lt_0: ∀a. ¬(a < 0)
  - notI %
  - gt_neq_0 1
  - falI refl 1 %

lemma conjE: ∀P Q R. P ∧ Q  ⟶  (P  ⟶  Q  ⟶  R)  ⟶  R
  - conjE1 1+
  - conjE2 1
  - 1 2 3 %

lemma lte_exh: ∀P a b. a <= b  ⟶  (a < b  ⟶  P)  ⟶  (a  = b  ⟶  P)  ⟶  P
  - psub lte_def 1*
  - disjE 1 %
  - 1 3 %
  - 2 3 %

lemma lte_tran: ∀ a b c. a <= b  ⟶  b <= c  ⟶  a <= c
  - lte_exh 1 %
  - lte_exh 1 %
  - lt_tran 1 2
  - lt_imp_lte 1 %
  sub 2
  - lt_imp_lte 1 %
  sub 2
  - 1 %

lemma lt_lte_tran: ∀a b c. a < b  ⟶  b <= c  ⟶  a < c
  - lte_exh 2 %
  - lt_tran 1 2 %
  sub 2
  - 1 %

lemma lte_lt_tran: ∀a b c. a <= b  ⟶  b < c  ⟶  a < c
  - lte_exh 1 %
  - lt_tran 2 1 %
  sub 2
  - 1 %

lemma exi_least: ∀P. (∃) P  ⟶  (∃n. P n ∧ (∀k. k < n  ⟶  ¬P k))
  ren a P
  - exiE 1 %
  ren a N
  - split[∃n. n < N ∧ P n ∧ (∀k. k < n  ⟶  ¬P k)] %
  - exiE 2 %
  ren a n
  - conjE2 2*+
  - conjE1 2*
  - conjE2 2*+
  - conjE1 2*
  show [(μn. P n ∧ (∀k. k < n  ⟶  ¬P k)) = n]
  - exiI[n] %
  - conjI %
  - 3 %
  ren a k
  - 4 6 %
  - muI %
  - conjI %
  - 3 %
  - 4 5 %
  ren a k
  - notI %
  - conjE1 6
  - 4*+ 5
  - falE2 6 5 %
  - dmrg_ne 2
  - exiI[N] %
  - conjI %
  - 1 %
  ren a n
  show [∀n. n < N  ⟶  P n  ⟶  ∃k. k < n ∧ P k]
  del 2
  - nat_ind_lte[λn. n < N  ⟶  ¬P n] %
  - notI %
  - 3 4 5
  - exiE 3 %
  del 2
  ren a n
  - conjE 2 %
  - falI 2 not_lt_0 %
  del 2
  ren a n
  - notI %
  - 2+ 4+ 5+
  - exiE 6 %
  ren a k
  - conjE 6 %
  - lt_suc_lte 6*
  - psub lte_suc2 6*
  - lte_lte_suc 6+
  - lte_lt_tran 8 4+
  - 3 6 8
  - falI 5 6 %
  - 2 %
  ren a k
  - 2*[k]
  - dmrg_nc 2*
  - conjI 4 5
  - notI2 4
  - disjE1 2* 4
  - dmrg_nu 2*
  - imp_swap subr 2 %
  - ext %
  - iffI %
  - conjE 3 %
  - notI %
  - 5 3
  - falI 3 4 %
  - cposr_np 3 %
  - dmrg_nc 3*
  - disjE 3 %
  - falE2 3 4 %
  - 4 %

lemma uniq_least: ∀P. (∃) P  ⟶  (∃!n. P n ∧ (∀k. k < n  ⟶  ¬P k))
  - exi_least 1
  - exiE 1 %
  - conjE 1 %
  ren a P
  ren b n₀
  - uniqI1[n₀] %
  - conjI %
  - 1 %
  ren a n₁
  - 2 3 %
  ren a n₁
  - conjE 3 %
  - iffI %
  - conjE 5 %
  - cmp[n₁, n₀] %
  - 4 7
  - falE2 4 6 %
  - 6 7
  - falE2 3 6 %
  - 7 %
  sub 5
  - conjI %
  - 3 %
  - 4 5 %

lemma muE: ∀P n. (μ) P = n  ⟶  (∃) P  ⟶  P n ∧ (∀k. k < n  ⟶  ¬P k)
  ren a P
  ren b n
  - uniq_least 2*
  let N: THE a. P a ∧ (∀b. b < a  ⟶  ¬P b)
  - uniqE 2+
  - conjE 4 %
  - subr 3+ 4*
  - subr[λx. ∀a. a < x  ⟶  ¬P a] 3+ {1}5
  show [(μ) P = N]
  - eq_tran2 1+ 6+
  sub 7
  - conjI 4 {1}5 %
  - muI %
  - 4 %
  - 5 6 %

lemma suc_least_gt: ∀a. (μb. a < b) = Suc a
  - muI %
  - lt_suc %
  - notI %
  - lt_suc_lte 2
  - lte_exh 2 %
  - lt_gt_fal 1 2 %
  - lt_imp_neq1 1*
  - falI 2 1 %

lemma nul_not_nnul: ∀a. nul a  ⟶  ¬(nnul a)
  - notI %
  - psub nnul_exi_cons 2
  - exiE 2 %
  - exiE 2 %
  sub 2
  - falI 1 nul_simp2p %

lemma not_nul_nnul: ∀a. ¬(nul a)  ⟶  nnul a
  - list_ind[λa. ¬nul a  ⟶  nnul a] %
  - falE2 nul_simp1p 2 %
  del 1
  - nnul_simp2p %
  - 1 %

lemma sp: ∀P Q R. (P  ⟶  Q  ⟶  R)  ⟶  Q  ⟶  P  ⟶  R
  - 1 3 2 %

lemma nnul_not_nul: ∀a. nnul a  ⟶  ¬(nul a)
  - cpos_pn nul_not_nnul 1 %

lemma not_nnul_nul: ∀a. ¬(nnul a)  ⟶  nul a
  - cpos_np not_nul_nnul 1 %

lemma nul_iff_nil: ∀a. nul a = (a = Nil)
  - list_ind[#..a] %
  - tranr1 nul_simp1 %
  - eq_truI refl %
  - tranr1 nul_simp2 %
  - eq_falI %
  - neq_com %
  - list_dif %

lemma nexi_gt_all: ¬∃a. ∀b. b < a
  - notI %
  - exiE 1 %
  - falI 1 not_lt_refl %

lemma lt_not_gte: ∀a b. (a < b) = ¬(b <= a)
  - iffI %
  - notI %
  - lte_exh 2 %
  - lt_gt_fal 1 2 %
  sub 2
  - falI 1 not_lt_refl %
  - sub lte_def 1
  - dmrg_nd 1
  - conjE 1 %
  - cmp[a, b] %
  - 3 %
  - falE2 3 1 %
  sub 3
  - falE2 refl 2 %

lemma nexi_gte_all: ¬∃a. ∀b. b <= a
  - notI %
  - exiE 1 %
  - nat_inf[a]
  - exiE 2 %
  - 1*[b]
  - psub lt_not_gte 2
  - falI 1 2 %

const foldr :: 'b  ⟹  ('a  ⟹  'b  ⟹  'b)  ⟹  list 'a  ⟹  'b

axiom foldr_simp1: ∀z f. foldr z f Nil = z
axiom foldr_simp2: ∀z f a b. foldr z f (Cons a b) = f a (foldr z f b)

def length: foldr 0 (λa b. Suc b)

lemma length_def1: ∀a. length a = foldr 0 (λa b. Suc b) a
  - fun_cong length_def %

lemma length_simps: ∀a b. length Nil = 0 ∧ length (Cons a b) = Suc (length b)
  - conjI %
  - tranr length_def1 %
  - tranr foldr_simp1 refl %
  - tranr length_def1 %
  - tranr foldr_simp2 %
  - arg_cong %
  - com length_def1 %

lemma length_simp1: length Nil = 0
  - conjE1 length_simps %

lemma length_simp2: ∀a b. length (Cons a b) = Suc (length b)
  - conjE2 length_simps %

lemma exi_exi: (∃) (∃)
  - exiI[univ] %
  - exiI[undefined] %
  - psub in_def all_in_univ %

lemma etaI: ∀P f. P f  ⟶  P (λa. f a)
  - com eta
  - arg_cong 2
  - psub 2 1 %

lemma not_all_all: ¬((∀) (∀))
  - notI %
  - etaI 1
  - 1[∅]
  - etaI 1
  - psubr in_def 1
  - falI 1 not_in_emp %

lemma all_eq_unit: ∀a. a = Unit
  - unit_ind[#..a] refl %

lemma unit_eq_all: ∀a. Unit = a
  - com all_eq_unit %

lemma exi_func_fst_snd: ∃f. ∀a b. f (Pair a b) = a ∧ f (Pair a b) = b
  - exiI[λx. (λx y. y) (fst x = Unit) Unit] %
  - conjI unit_eq_all unit_eq_all %

spacing (FIX) 0 1 0
def FIX [binder]: λf. THE x. f x = x

lemma fix_def: ∀f. (FIX) f = THE x. f x = x
  - fun_cong FIX_def %

def id₁: FIX f. λx. if (x = 0) 0 (Suc (f (pred x)))

lemma id₁_eq_id: id₁ = id
  - tranr id₁_def %
  - tranr fix_def %
  - theI %
  - ext %
  - com %
  - tranr1 id_def1 %
  - if_eq %
  - com 1 %
  - psub neq_0_exi_suc 1
  - exiE 1 %
  sub 1
  - arg_cong %
  - tranr id_def1 pred_suc %
  ren a f
  - fun_cong 1
  - ext %
  - com %
  - tranr1 id_def1 %
  ren a n
  - nat_ind[#..n] %
  - if_tru_t1 1 refl
  - com 1 %
  ren a n
  - if_fal_t1 1* suc_neq_0 [n]
  - sub[λx. Suc (f x) = f (Suc n)] pred_suc 1*
  - sub[λx. Suc x = f (Suc n)] 2+ 1*
  - com 1 %

def pred₁: λn. if (n = 0) 0 (pred n)

lemma pred1_def: ∀n. pred₁ n = if (n = 0) 0 (pred n)
  - fun_cong pred₁_def %

lemma fix_pred₁_eq_0: (FIX) pred₁ = 0
  - tranr fix_def %
  - theI %
  - tranr pred1_def %
  - if_tru_t refl %
  ren a n
  - notE2 %
  - psub neq_0_exi_suc 2
  - exiE 2 %
  sub 2
  ren a n
  - tran pred1_def 1
  - if_fal_t1 1 suc_neq_0
  - eq_tran2 pred_suc 1
  - falI 1 neq_suc %

lemma set_eq': ∀a b. (∀c. c ∈ a = c ∈ b)  ⟶  a = b
  - ext %
  - 1[c]
  - tran1 in_def 1
  - tran1 in_def 1 %

lemma set_eq: ∀a b. (a = b) = ((∀c. c ∈ a = c ∈ b) ∧ (∀c. a ∈ c = b ∈ c))
  - iffI %
  sub 1
  - conjI %
  - refl %
  - refl %
  - conjE1 1
  - set_eq' {1}1 %

def (⋂) [infixl 55]: λa b c. c ∈ a ∧ c ∈ b
def (⋃) [infixl 55]: λa b c. c ∈ a ∨ c ∈ b

lemma cap_def: ∀a b. a ⋂ b = λc. c ∈ a ∧ c ∈ b
  - fun_cong2 ⋂_def %

lemma cup_def: ∀a b. a ⋃ b = λc. c ∈ a ∨ c ∈ b
  - fun_cong2 ⋃_def %

lemma lem_z3_5438: ∀x y. (∀Q. x ∈ Q  ⟶  y ∈ Q)  ⟶  x = y
  ren a x
  ren b y
  - 1[λz. z = x]
  - psubr in_def
  - imp_tran 2 1 refl
  - psub in_def 1
  - com 1 %

def map: λf. foldr Nil (λx. Cons (f x))

lemma map_def1: ∀f xs. map f xs = foldr Nil (λx. Cons (f x)) xs
  - fun_cong2 map_def %

lemma map_simp1: ∀f. map f Nil = Nil
  - tranr map_def1 %
  - tranr foldr_simp1 refl %

lemma map_simp2: ∀f x xs. map f (Cons x xs) = Cons (f x) (map f xs)
  - tranr map_def1 %
  - tranr foldr_simp2 %
  - arg_cong %
  - tran map_def1 refl %

lemma fsub: ∀a b c f. a = b  ⟶  f a = c  ⟶  f b = c
  sub 1
  - 1 %

lemma fsubr: ∀a b c f. a = b  ⟶  f b = c  ⟶  f a = c
  sub 1
  - 1 %

lemma fsub1: ∀a b c f. f a = c  ⟶  a = b  ⟶  f b = c
  - fsub 2 1 %

lemma fsubr1: ∀a b c f. f b = c  ⟶  a = b  ⟶  f a = c
  - fsubr 2 1 %

lemma map_prsv_len: ∀xs f. length (map f xs) = length xs
  ren a xs
  ren b f
  - list_ind[#..xs] %
  - arg_cong map_simp1 %
  - fsubr map_simp2 %
  - tranr1 length_simp2 %
  - tranr1 length_simp2 %
  - arg_cong 1 %

def last': λxs. foldr (Pair False undefined) (λx p. if (fst p) p (Pair True x)) xs
def last: λxs. snd (last' xs)

lemma last'_def1: ∀xs. last' xs = foldr (Pair False undefined) (λx p. if (fst p) p (Pair True x)) xs
  - fun_cong last'_def %

lemma last_last': ∀xs. last xs = snd (last' xs)
  - fun_cong last_def %

lemma last_def1: ∀xs. last xs = snd (foldr (Pair False undefined) (λx p. if (fst p) p (Pair True x)) xs)
  - tranr last_last' %
  - arg_cong last'_def1 %

lemma if_tru_subr: ∀P a b c. a  ⟶  P b  ⟶  P (if a b c)
  - sub1 2 %
  - com %
  - if_tru_r1 1 refl %

lemma if_fal_subr: ∀P a b c. ¬a  ⟶  P c  ⟶  P (if a b c)
  - sub1 2 %
  - com %
  - if_fal_r1 1  refl %

lemma if_tru_fsubr: ∀a b c d f. a  ⟶  f b = d  ⟶  f (if a b c) = d
  - fsub1 2 %
  - com %
  - if_tru_r1 1 refl %

lemma if_fal_fsubr: ∀a b c d f. ¬a  ⟶  f c = d  ⟶  f (if a b c) = d
  - fsub1 2 %
  - com %
  - if_fal_r1 1 refl %

lemma last'_cons_tru: ∀x xs. fst (last' (Cons x xs))
  ren a x
  ren b xs
  - list_ind[λxs. ∀x. fst (last' (Cons x xs))] %
  ren a x
  - subr last'_def1 %
  - subr foldr_simp2 %
  - if_fal_subr %
  - notI %
  - sub foldr_simp1 1
  - psub fst_simp 1 %
  - psubr fst_simp true %
  ren a y
  ren b ys
  ren c x
  - subr last'_def1 %
  - subr foldr_simp2 %
  - if_tru_subr %
  - sub last'_def1 1 %
  - sub last'_def1 1 %

lemma last'_simp1: ∀x. last' (Cons x Nil) = Pair True x
  ren a x
  - tranr last'_def1 %
  - tranr foldr_simp2 %
  - if_fal_r1 %
  - notI %
  - sub foldr_simp1 1
  - psub fst_simp 1 %
  - refl %

lemma last'_simp2: ∀x y ys. last' (Cons x (Cons y ys)) = last' (Cons y ys)
  ren a x
  ren b y
  ren c ys
  - list_ind[λys. ∀x y. last' (Cons x (Cons y ys)) = last' (Cons y ys)] %
  ren a x
  ren b y
  - tranr last'_def1 %
  - tranr foldr_simp2 %
  - if_tru_r1 %
  - subr foldr_simp2 %
  - if_fal_subr %
  - notI %
  - sub foldr_simp1 1
  - psub fst_simp 1 %
  - psubr fst_simp true %
  - tran last'_def1 refl %
  ren a z
  ren b zs
  ren c x
  ren d y
  - tranr last'_def1 %
  - tranr foldr_simp2 %
  - if_tru_r1 %
  - sub last'_def1 last'_cons_tru %
  - tranr foldr_simp2 %
  - if_tru_r1 %
  - sub last'_def1 last'_cons_tru %
  - tran last'_def1 %
  - com 1 %

lemma last_simp1: ∀x. last (Cons x Nil) = x
  ren a x
  - tranr last_def1 %
  - imp_swap fsubr snd_simp
  show [∀a. a = Pair True x  ⟶  snd a = x]
  del 1
  - 1 %
  - tranr foldr_simp2 %
  - if_fal_r1 %
  - notI %
  - sub foldr_simp1 1
  - psub fst_simp 1 %
  - refl %
  sub 2
  - snd_simp %

lemma last_simp2: ∀x y ys. last (Cons x (Cons y ys)) = last (Cons y ys)
  ren a x
  ren b y
  ren c ys
  - tranr1 last_last' %
  - tranr1 last_last' %
  - arg_cong last'_simp2 %

lemma tr1: ∀a₁ b₁ f x y. f a₁ = x  ⟶  b₁ = a₁  ⟶  x = y  ⟶  f b₁ = y
  sub 2
  - tranr 1 2 %

lemma tr2: ∀a₁ a₂ b₁ b₂ f x y. f a₁ a₂ = x  ⟶  b₁ = a₁  ⟶  b₂ = a₂  ⟶  x = y  ⟶  f b₁ b₂ = y
  sub 2
  sub 2
  - tranr 1 2 %

lemma tr3: ∀a₁ a₂ a₃ b₁ b₂ b₃ f x y. f a₁ a₂ a₃ = x  ⟶  b₁ = a₁  ⟶  b₂ = a₂  ⟶  b₃ = a₃  ⟶  x = y  ⟶  f b₁ b₂ b₃ = y
  sub 2
  sub 2
  sub 2
  - tranr 1 2 %

def const: λa b. a

lemma const_def1: ∀a b. const a b = a
  - fun_cong2 const_def %

def const_f: λf. ∀x y. f x = f y

lemma const_f_def1: ∀f. const_f f = (∀x y. f x = f y)
  - fun_cong const_f_def %

lemma conf_f_const: ∀a. const_f (const a)
  - psubr const_f_def1 %
  - tranr1 const_def1 %
  - tranr1 const_def1 refl %

def replicate: λa. nat_fold Nil (Cons a)

lemma replicate_def1: ∀a n. replicate a n = nat_fold Nil (Cons a) n
  - fun_cong2 replicate_def %

lemma replicate_simp1: ∀a. replicate a 0 = Nil
  - tranr replicate_def1 %
  - nat_fold_simp1 %

lemma replicate_simp2: ∀a n. replicate a (Suc n) = Cons a (replicate a n)
  ren a n
  ren b a
  - tranr replicate_def1 %
  - tranr nat_fold_simp2 %
  - arg_cong %
  - com replicate_def1 %

lemma len_replicate: ∀a n. length (replicate a n) = n
  ren b n
  - nat_ind[#..n] %
  - tr1 length_simp1 replicate_simp1 refl %
  - fsubr replicate_simp2 %
  - tranr length_simp2 %
  - arg_cong 1 %

lemma map_const_f: ∀f. const_f f  ⟶  ∃g. ∀xs. map f xs = g (length xs)
  ren a f
  - exiI[replicate (f undefined)] %
  ren a xs
  - psub const_f_def1 1
  let a: f undefined
  - tranr 2 1
  - com 1
  - subr[λa. map f xs = replicate a (length xs)] 1+ %
  - list_ind[#..xs] %
  - tranr1 map_simp1 %
  - tr2 replicate_simp1 refl length_simp1 refl %
  ren b x
  ren c xs
  - tranr1 map_simp2 %
  - subr[λb. replicate a b = Cons (f x) (map f xs)] length_simp2 %
  - tranr replicate_simp2 %
  - cong %
  - com %
  - arg_cong 1 %
  - com 2 %

lemma foldr_const_f: ∀z f. const_f f  ⟶  ∃g. ∀xs. foldr z f xs = g (length xs)
  ren a z
  ren b f
  - exiI[nat_fold z (f undefined)] %
  ren a xs
  - psub const_f_def1 1
  let a: f undefined
  - tranr 2 1
  - com 1
  - subr[λa. foldr z f xs = nat_fold z a (length xs)] 1+ %
  - list_ind[#..xs] %
  - tranr1 foldr_simp1 %
  - tr3 nat_fold_simp1 refl refl length_simp1 refl %
  ren b x
  ren c xs
  - tranr1 foldr_simp2 %
  - subr[λb. nat_fold z a b = f x (foldr z f xs)] length_simp2 %
  - tranr nat_fold_simp2 %
  - cong %
  - com 1 %
  - com 2 %

lemma eta2: ∀P f. P (λa. f a)  ⟶  P f
  - imp_swap sub 1 %
  - ext %
  - refl %

lemma list_exh: ∀P. P Nil  ⟶  (∀x xs. P (Cons x xs))  ⟶  (∀) P
  ren a P
  - eta2 %
  ren a xs
  - list_ind[#..xs] %
  - 1 %
  - 2 %

lemma nat_exh: ∀P. P 0  ⟶  (∀n. P n)  ⟶  (∀) P
  ren a P
  - eta2 %
  ren a n
  - nat_ind[#..n] %
  - 1 %
  - 2 %

lemma nat_fold_simp_it: ∀z f n. nat_fold z f (Suc n) = nat_fold (f z) f n
  ren a z
  ren b f
  ren c n
  - nat_ind[λn. ∀z f. nat_fold z f (Suc n) = nat_fold (f z) f n] %
  ren a z
  ren b f
  - tranr nat_fold_simp2 %
  - fsubr nat_fold_simp1 %
  - com nat_fold_simp1 %
  ren a n
  ren b z
  ren c f
  - tranr1 nat_fold_simp2 %
  - tranr1 nat_fold_simp2 %
  - arg_cong 1 %

lemma nat_fold_replicate_tail: ∀a n. nat_fold (replicate a n) tail n = Nil
  ren b n
  - nat_ind[#..n] %
  - tranr nat_fold_simp1 %
  - replicate_simp1 %
  ren b n
  - subr[λx. nat_fold x tail (Suc n) = Nil] replicate_simp2 %
  - tranr nat_fold_simp_it %
  - tr3 1 tail_simp refl refl refl %

lemma nat_fold_tail_len: ∀xs. nat_fold xs tail (length xs) = Nil
  ren a xs
  - list_ind[#..xs] %
  - tr3 nat_fold_simp1 refl refl length_simp1 refl %
  ren a x
  ren b xs
  - subr[λa. nat_fold (Cons x xs) tail a = Nil] length_simp2 %
  - tranr nat_fold_simp_it %
  - tr3 1 tail_simp refl refl refl %

lemma nnul_cons: ∀x xs. nnul (Cons x xs)
  ren a x
  ren b xs
  - eq_truE nnul_simp2 %
lemma not_nnul_imp_nul: ∀xs. ¬(nnul xs)  ⟶  nul xs
  ren a xs
  - sub nnul_def1 1
  - notE 1
  sub 1
  - psubr nul_def1 refl %

lemma nat_fold_tail_lt_len: ∀xs n. n < length xs  ⟶  nnul (nat_fold xs tail n)
  ren a xs
  ren b n
  - nat_ind[λn. ∀xs. n < length xs  ⟶  nnul (nat_fold xs tail n)] %
  del 1
  ren a xs
  - list_exh[λxs. 0 < length xs  ⟶  nnul (nat_fold xs tail 0)] %
  del 1
  - sub[λa. 0 < a] length_simp1 1
  - falE2 1 not_lt_refl %
  del 1
  ren a x
  ren b xs
  - subr nat_fold_simp1 %
  - nnul_cons %
  - 1 %
  del 1
  ren a n
  ren b xs
  - subr nat_fold_simp_it %
  show [∃y ys. xs = Cons y ys]
  - exiE 3 %
  - exiE 3 %
  sub 3
  ren a x
  ren b xs
  - subr[λa. nnul (nat_fold a tail n)] tail_simp %
  - sub[λa. Suc n < a] length_simp2 2
  - psub lt_simp3 2
  - 1 2 %
  show [nnul xs]
  - psub nnul_exi_cons 3 %
  - notE2 %
  - not_nnul_imp_nul 3
  - psub nul_def1 3
  sub 3
  - sub[λa. Suc n < a] length_simp1 2
  - falE2 2 not_lt_0 %
  - 1 %

lemma nnul_imp_neq_nil: ∀xs. nnul xs  ⟶  ¬(xs = Nil)
  ren a xs
  - psub nnul_def1 1 %

lemma length_least_fold_tail: ∀xs. length xs = μn. nat_fold xs tail n = Nil
  ren a xs
  - com %
  - muI %
  - nat_fold_tail_len %
  ren a n
  - nat_fold_tail_lt_len 1
  - nnul_imp_neq_nil 1 %

def (++) [infixl 55]: λxs ys. foldr ys Cons xs

lemma append_def1: ∀xs ys. xs ++ ys = foldr ys Cons xs
  - fun_cong2 ++_def %

lemma map_id: ∀xs. map id xs = xs
  ren a xs
  - list_ind[#..xs] %
  - map_simp1 %
  ren a x
  ren b xs
  - tranr map_simp2 %
  - tr2 refl id_def1 1 refl %

lemma fold_cons: ∀xs. foldr Nil Cons xs = xs
  ren a xs
  - list_ind[#..xs] %
  - foldr_simp1 %
  ren a x
  ren b xs
  - tranr foldr_simp2 %
  - arg_cong 1 %

lemma append_simp1: ∀xs. Nil ++ xs = xs
  ren a xs
  - tranr append_def1 %
  - foldr_simp1 %

lemma append_nil: ∀xs. xs ++ Nil = xs
  ren a xs
  - tranr append_def1 fold_cons %

lemma append_simp2: ∀x xs ys. Cons x xs ++ ys = Cons x (xs ++ ys)
  ren a x
  ren b xs
  ren c ys
  - tranr append_def1 %
  - tranr foldr_simp2 %
  - arg_cong %
  - com append_def1 %

lemma append_len: ∀xs ys. length (xs ++ ys) = length xs + length ys
  ren a xs
  ren b ys
  - list_ind[#..xs] %
  - fsubr append_simp1 %
  - com %
  - tr2 add0r length_simp1 refl refl %
  ren a x
  ren b xs
  - fsubr append_simp2 %
  - tranr1 length_simp2 %
  - tr2 suc_add length_simp2 refl %
  - arg_cong %
  - com 1 %

def reverse: foldr Nil (λx xs. xs ++ Cons x Nil)

lemma reverse_def1: ∀xs. reverse xs = foldr Nil (λx xs. xs ++ Cons x Nil) xs
  - fun_cong reverse_def %

lemma reverse_simp1: reverse Nil = Nil
  - tranr reverse_def1 %
  - foldr_simp1 %

lemma reverse_simp2: ∀x xs. reverse (Cons x xs) = reverse xs ++ Cons x Nil
  ren a x
  ren b xs
  - tranr reverse_def1 %
  - tranr foldr_simp2 %
  - com reverse_def1
  - tr2 refl 1 refl refl %

lemma append_cons: ∀xs y ys. xs ++ (Cons y ys) = xs ++ (Cons y Nil) ++ ys
  ren a xs
  ren b y
  ren c ys
  - list_ind[#..xs] %
  - tranr1 append_simp1 %
  - tr2 append_simp2 append_simp1 refl %
  - arg_cong append_simp1 %
  ren a x
  ren b xs
  - tranr1 append_simp2 %
  - tr2 append_simp2 append_simp2 refl %
  - arg_cong %
  - com 1 %

lemma append_assoc: ∀xs ys zs. xs ++ ys ++ zs = xs ++ (ys ++ zs)
  ren a xs
  ren b ys
  ren c zs
  - list_ind[#..xs] %
  - tr2 refl append_simp1 refl %
  - com %
  - append_simp1 %
  ren a x
  ren b xs
  - com %
  - tranr1 append_simp2 %
  - tr2 append_simp2 append_simp2 refl %
  - arg_cong 1 %

lemma reverse_append: ∀xs ys. reverse (xs ++ ys) = reverse ys ++ reverse xs
  ren a xs
  ren b ys
  - list_ind[#..xs] %
  - fsubr append_simp1 %
  - com %
  - tr2 append_nil refl reverse_simp1 refl %
  ren a x
  ren b xs
  - fsubr append_simp2 %
  - tranr reverse_simp2 %
  - tr2 refl 1 refl %
  - com %
  - tr2 refl refl reverse_simp2 %
  - com append_assoc %

lemma length_append: ∀xs ys. length (xs ++ ys) = length xs + length ys
  ren a xs
  ren b ys
  - list_ind[#..xs] %
  - fsubr append_simp1 %
  - com %
  - tr2 add0r length_simp1 refl refl %
  ren a x
  ren b xs
  - fsubr append_simp2 %
  - tranr1 length_simp2 %
  - tr2 suc_add length_simp2 refl %
  - arg_cong %
  - com 1 %

lemma length_reverse: ∀xs. length (reverse xs) = length xs
  ren a xs
  - list_ind[#..xs] %
  - tr1 length_simp1 reverse_simp1 %
  - com length_simp1 %
  ren a x
  ren b xs
  - com %
  - tranr1 length_simp2 %
  - fsubr reverse_simp2 %
  - tranr length_append %
  - tr2 add_simp2 1 length_simp2 %
  - arg_cong %
  - tr2 add_simp1 refl length_simp1 refl %

lemma reverse_single: ∀x. reverse (Cons x Nil) = Cons x Nil
  ren a x
  - tranr reverse_simp2 %
  - tr2 append_simp1 reverse_simp1 refl refl %

lemma reverse2: ∀xs. reverse (reverse xs) = xs
  ren a xs
  - list_ind[#..xs] %
  - tr1 reverse_simp1 reverse_simp1 refl %
  ren a x
  ren b xs
  - fsubr reverse_simp2 %
  - tranr reverse_append %
  - tr2 append_simp2 reverse_single 1 %
  - arg_cong append_simp1 %

def foldl: λz f xs. foldr z (λx xs. f xs x) (reverse xs)

lemma foldl_def1: ∀z f xs. foldl z f xs = foldr z (λx xs. f xs x) (reverse xs)
  - fun_cong2 foldl_def
  - fun_cong 1 %

lemma foldl_simp1: ∀z f. foldl z f Nil = z
  ren a z
  ren b f
  - tranr foldl_def1 %
  - tr3 foldr_simp1 refl refl reverse_simp1 refl %

lemma append_reverse: ∀xs ys. xs ++ ys = reverse (reverse ys ++ reverse xs)
  - arg_cong[reverse] reverse_append
  - tran reverse2 1 %

lemma append_reverse_single: ∀x xs. reverse xs ++ (Cons x Nil) = reverse (Cons x xs)
  ren a x
  ren b xs
  - com %
  - tranr reverse_simp2 refl %

lemma foldr_append_single: ∀z f x xs. foldr z f (xs ++ Cons x Nil) = foldr (f x z) f xs
  ren a z
  ren b f
  ren c x
  ren d xs
  - list_ind[#..xs] %
  - tr3 foldr_simp2 refl refl append_simp1 %
  - com %
  - tranr1 foldr_simp1 %
  - arg_cong foldr_simp1 %
  ren a y
  ren b ys
  - tr3 foldr_simp2 refl refl append_simp2 %
  - tr2 refl refl 1 %
  - com %
  - tranr foldr_simp2 refl %

lemma foldl_simp2: ∀z f x xs. foldl z f (Cons x xs) = foldl (f z x) f xs
  ren a z
  ren b f
  ren c x
  ren d xs
  - tranr1 foldl_def1 %
  - tranr1 foldl_def1 %
  let g: λa b. f b a
  - com 1+
  - fun_cong2 2+
  - tr3 refl refl 2+ refl %
  - com %
  - tr3 refl 3 2 refl %
  - com %
  del 1
  let ys: reverse xs
  - tr3 refl refl refl reverse_simp2 %
  - sub[λa. foldr z g (a ++ Cons x Nil) = foldr (g x z) g a] 1 %
  - foldr_append_single %

Implementation

Implementation - If it's not on the master, check the commit history.

Retrieved from "https://esolangs.org/w/index.php?title=Тест_на_терпение&oldid=93272"