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

From Esolang
(Redirected from Patience test)
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"