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

Тест на терпение 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.
Category:Languages
Category:2020
Category:Implemented