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

Paradigm(s) Declarative User:Hakerh400 2020 Not applicable Implementation in JavaScript `.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 nat_fold_simp1 refl %

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

lemma add0: ∀a. a + 0 = a

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

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

lemma add_com: ∀a b. a + b = b + a
- nat_ind[λa. ∀b. a + b = b + a] %
ren c a
ren d b
- com %
- 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
del 1
ren d a
ren e b
ren f c
- Suc_inj 2
- 1 2 %
- 1 %

lemma add_inj: ∀a. inj ((+) a)

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
- arg_cong %
ren d a
ren e b
ren f c
- subr[λx. b + x = Suc (b + c + a)] add_simp2 %
- arg_cong 1 %

lemma lte_add: ∀a b. a <= a + b
- nat_ind[λb. ∀a. a <= a + b] %
- 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] %
sub 1
- iffI %
- com 1
sub 1
- arg_cong %
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 %
- arg_cong %
- com 2 %
- iffI %
- com 4
- Suc_inj 4
- com 4
sub 4
- uniqE 1+
- com %
- 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
del 1
ren c b
- 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

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

- 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
- theE 1+
- subr[#..sub] sub_def %
- conjI %
- 2+[0, a] gte_0
- uniqE 4
- com 4
- arg_cong %
- ext %
- iffI %
- com 4
- Suc_inj 4
- com 4 %
sub 4
- com %

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.