Normalization of the simply typed lambda calculus

TheoremMulti-step evaluation is a congruence in function position#✓fully proved

Let \(f\) and \(f'\) be terms of type \(A \Rightarrow B\) and let \(a\) be a term of type \(A\), all in the same context. If \(f\) evaluates to \(f'\) in zero or more call-by-value steps, then the application \(f\,a\) evaluates to \(f'\,a\) in zero or more steps.

theorem appFun {f f' : Tm Γ (A ⇒ B)} (a : Tm Γ A) (h : Steps f f') :
    Steps (.app f a) (.app f' a)

Uses 4 · Used by 4

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSmall-step call-by-value reduction in STLC

Used byReducibility is closed under backward evaluation · Application preserves having the same result · Reducibility is closed under forward evaluation · Big-step evaluation implies small-step evaluation

TheoremEvaluating the argument of a value function is a multi-step congruence#✓fully proved

Let \(f\) be a term of type \(A \Rightarrow B\) and let \(a\), \(a'\) be terms of type \(A\), all in the same context. If \(f\) is a value and \(a\) evaluates to \(a'\) in zero or more call-by-value steps, then the application \(f\,a\) evaluates to \(f\,a'\) in zero or more steps.

theorem appArg {a a' : Tm Γ A} {f : Tm Γ (A ⇒ B)} (hv : Value f) (h : Steps a a') :
    Steps (.app f a) (.app f a')

Uses 5 · Used by 3

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesSmall-step call-by-value reduction in STLC

Used byApplication preserves having the same result · Fundamental theorem of the reducibility relation · Big-step evaluation implies small-step evaluation

TheoremEvaluation to a value passes through every reduct#✓fully proved

Let \(t\), \(t'\) and \(v\) be terms of the same type in the same context, with \(v\) a value. If \(t\) evaluates to \(v\) and \(t\) evaluates to \(t'\), each in finitely many call-by-value steps, then \(t'\) evaluates to \(v\) in finitely many steps.

The value endpoint makes the first evaluation maximal, so every other finite evaluation is one of its prefixes.

theorem suffix_of_value {t t' v : Tm Γ A} (htv : Steps t v) (hv : Value v)
    (htt' : Steps t t') : Steps t' v

Uses 7 · Used by 2

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesSmall-step call-by-value reduction in STLC · Small-step call-by-value reduction in STLC is deterministic · Values are irreducible

Used byTermination is closed under forward evaluation · Uniqueness of the value reached by evaluation

DefinitionTermination of closed terms#✓fully proved

A closed term \(t\) terminates when it evaluates, in finitely many call-by-value steps, to a value.

def Terminates (t : Tm [] A) : Prop := ∃ v, Steps t v ∧ Value v

Uses 4 · Used by 18

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Used byTermination is closed under backward evaluation · Reducibility is closed under backward evaluation · Application preserves having the same result · Closed functions evaluate to lambda abstractions · Termination is closed under forward evaluation · Reducibility is closed under forward evaluation · Fundamental theorem of the reducibility relation · Normalization and termination coincide · No closed terms of base type · Normalization of closed terms · Evaluation preserves the result of a closed term · Values terminate · Tait reducibility for closed terms · Reflexivity of having the same result · Reducible terms terminate · Termination of the call-by-value simply typed lambda calculus · Closed simply typed terms have a big-step evaluation · Termination in terms of big-step evaluation

TheoremValues terminate#✓fully proved

Every closed term of the simply typed lambda calculus that is a value terminates.

No evaluation step is needed: the value itself is the value reached.

theorem of_value {v : Tm [] A} (hv : Value v) : Terminates v

Uses 6 · Used by 1

Statement usesTermination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesSmall-step call-by-value reduction in STLC · Multi-step call-by-value reduction in STLC

Used byFundamental theorem of the reducibility relation

TheoremTermination is closed under backward evaluation#✓fully proved

Let \(t\) and \(t'\) be closed terms of the same type. If \(t\) evaluates to \(t'\) in zero or more call-by-value steps and \(t'\) terminates, then \(t\) terminates.

theorem anti {t t' : Tm [] A} (h : Steps t t') (ht' : Terminates t') : Terminates t

Uses 6 · Used by 1

Statement usesMulti-step call-by-value reduction in STLC · Termination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSmall-step call-by-value reduction in STLC · Values of STLC

Used byReducibility is closed under backward evaluation

TheoremTermination is closed under forward evaluation#✓fully proved

Let \(t\) and \(t'\) be closed terms of the same type. If \(t\) terminates and \(t\) evaluates to \(t'\) in zero or more call-by-value steps, then \(t'\) terminates.

theorem forward {t t' : Tm [] A} (ht : Terminates t) (h : Steps t t') : Terminates t'

Uses 6 · Used by 1

Statement usesMulti-step call-by-value reduction in STLC · Termination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesEvaluation to a value passes through every reduct · Values of STLC

Used byReducibility is closed under forward evaluation

DefinitionTait reducibility for closed terms#✓fully proved

Reducibility of a closed term \(t\) is defined by recursion on its simple type. At a base type, \(t\) is reducible when it terminates. At a function type \(A \Rightarrow B\), \(t\) is reducible when it terminates and, for every reducible closed term \(a\) of type \(A\), the application \(t\,a\) is reducible.

def Reducible : {A : Ty Base} → Tm [] A → Prop
  | .base _, t => Terminates t
  | .arr A _B, f =>
      Terminates f ∧ ∀ (a : Tm [] A), Reducible a → Reducible (.app f a)

Uses 3 · Used by 9

Statement usesTermination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Used byReducibility is closed under backward evaluation · Extending a reducible substitution by a reducible term keeps it reducible · Substitutions on the empty context are reducible · Reducibility is closed under forward evaluation · Fundamental theorem of the reducibility relation · Reducibility is invariant under evaluation · Closed terms are reducible · Reducible substitutions · Reducible terms terminate

TheoremReducible terms terminate#✓fully proved

Every reducible closed term of the simply typed lambda calculus terminates.

theorem terminates : {A : Ty Base} → {t : Tm [] A} → Reducible t → Terminates t

Uses 4 · Used by 2

Statement usesTait reducibility for closed terms · Termination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Used byFundamental theorem of the reducibility relation · Termination of the call-by-value simply typed lambda calculus

TheoremReducibility is closed under forward evaluation#✓fully proved

Let \(t\) and \(t'\) be closed terms of the same type. If \(t\) is reducible and \(t\) evaluates to \(t'\) in zero or more call-by-value steps, then \(t'\) is reducible.

theorem forward : {A : Ty Base} → {t t' : Tm [] A} →
    Steps t t' → Reducible t → Reducible t'

Uses 7 · Used by 2

Statement usesTait reducibility for closed terms · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesMulti-step evaluation is a congruence in function position · Termination of closed terms · Termination is closed under forward evaluation

Used byFundamental theorem of the reducibility relation · Reducibility is invariant under evaluation

TheoremReducibility is closed under backward evaluation#✓fully proved

Let \(t\) and \(t'\) be closed terms of the same type. If \(t\) evaluates to \(t'\) in zero or more call-by-value steps and \(t'\) is reducible, then \(t\) is reducible.

theorem anti : {A : Ty Base} → {t t' : Tm [] A} →
    Steps t t' → Reducible t' → Reducible t

Uses 7 · Used by 2

Statement usesTait reducibility for closed terms · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesMulti-step evaluation is a congruence in function position · Termination of closed terms · Termination is closed under backward evaluation

Used byFundamental theorem of the reducibility relation · Reducibility is invariant under evaluation

TheoremReducibility is invariant under evaluation#✓fully proved

Let \(t\) and \(t'\) be closed terms of the same type. If \(t\) evaluates to \(t'\) in zero or more call-by-value steps, then \(t\) is reducible if and only if \(t'\) is reducible.

theorem iff_of_steps {t t' : Tm [] A} (h : Steps t t') : Reducible t ↔ Reducible t'

Uses 6

Statement usesTait reducibility for closed terms · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesReducibility is closed under backward evaluation · Reducibility is closed under forward evaluation

DefinitionReducible substitutions#✓fully proved

A substitution \(\sigma\) that replaces each variable of a context \(\Gamma\) by a closed term of the same type is reducible when \(\sigma(x)\) is reducible for every variable \(x\) of \(\Gamma\).

def ReducibleSub (σ : Sub Γ []) : Prop := ∀ {A} (x : Var Γ A), Reducible (σ x)

Uses 4 · Used by 3

Statement usesTait reducibility for closed terms · Simultaneous substitutions of simply typed contexts · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byExtending a reducible substitution by a reducible term keeps it reducible · Substitutions on the empty context are reducible · Fundamental theorem of the reducibility relation

TheoremSubstitutions on the empty context are reducible#✓fully proved

Every substitution from the empty context to closed terms is reducible, since the empty context has no variables.

theorem empty (σ : Sub ([] : List (Ty Base)) []) : ReducibleSub σ

Uses 5 · Used by 1

Statement usesReducible substitutions · Simultaneous substitutions of simply typed contexts · Simple types

Proof usesTait reducibility for closed terms · Typed de Bruijn variables of the simply typed lambda calculus

Used byClosed terms are reducible

TheoremExtending a reducible substitution by a reducible term keeps it reducible#✓fully proved

Let \(\sigma\) be a substitution that sends each variable of a context \(\Gamma\) to a closed term of the same type, and let \(a\) be a closed term of type \(A\). If \(\sigma\) and \(a\) are reducible, then so is the substitution on the context \(A, \Gamma\) that sends the newest variable to \(a\) and each older variable \(x\) to \(\sigma(x)\).

theorem cons {σ : Sub Γ []} (hσ : ReducibleSub σ) {a : Tm [] A} (ha : Reducible a) :
    ReducibleSub (Sub.cons a σ)

Uses 7 · Used by 1

Statement usesTait reducibility for closed terms · Reducible substitutions · Simultaneous substitutions of simply typed contexts · Extension of a simply typed substitution · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesTyped de Bruijn variables of the simply typed lambda calculus

Used byFundamental theorem of the reducibility relation

TheoremFundamental theorem of the reducibility relation#✓fully proved

Let \(t\) be a term of type \(A\) in a context \(\Gamma\), and let \(\sigma\) be a reducible substitution sending each variable of \(\Gamma\) to a closed term of the same type. Then the closed term obtained by applying \(\sigma\) to \(t\) is reducible.

The lambda case is the key: evaluate an arbitrary reducible argument to a value, cross the beta step, and invoke the induction hypothesis under the extended substitution.

theorem fundamental (t : Tm Γ A) (σ : Sub Γ []) (hσ : ReducibleSub σ) :
    Reducible (Tm.subst σ t)

Uses 21 · Used by 1

Statement usesTait reducibility for closed terms · Reducible substitutions · Simultaneous substitutions of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Simultaneous substitution (simply typed lambda calculus) · Simple types

Proof usesReducibility is closed under backward evaluation · Reducibility is closed under forward evaluation · Reducible terms terminate · Extending a reducible substitution by a reducible term keeps it reducible · Small-step call-by-value reduction in STLC · Multi-step call-by-value reduction in STLC · Evaluating the argument of a value function is a multi-step congruence · Extension of a simply typed substitution · Lifting a substitution under a binder (simply typed lambda calculus) · Termination of closed terms · Values terminate · Instantiating a binder body (simply typed lambda calculus) · Substituting by an extended substitution, via lifting · Values of STLC · Typed de Bruijn variables of the simply typed lambda calculus

Used byClosed terms are reducible

TheoremClosed terms are reducible#✓fully proved

Every closed well-typed term of the simply typed lambda calculus is reducible.

theorem reducible_closed (t : Tm [] A) : Reducible t

Uses 11 · Used by 1

Statement usesTait reducibility for closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSubstitutions on the empty context are reducible · Simultaneous substitutions of simply typed contexts · Identity substitution (simply typed lambda calculus) · Lifting a substitution under a binder (simply typed lambda calculus) · Simultaneous substitution (simply typed lambda calculus) · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Fundamental theorem of the reducibility relation

Used byTermination of the call-by-value simply typed lambda calculus

TheoremTermination of the call-by-value simply typed lambda calculus#✓fully proved

Every closed well-typed term evaluates, in finitely many call-by-value steps, to a value.

theorem terminates_closed (t : Tm [] A) : Terminates t

Uses 5 · Used by 7

Statement usesTermination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesReducible terms terminate · Closed terms are reducible

Used byApplication preserves having the same result · Closed functions evaluate to lambda abstractions · No closed terms of base type · Normalization of closed terms · Evaluation preserves the result of a closed term · Reflexivity of having the same result · Closed simply typed terms have a big-step evaluation

TheoremValues reduce only to themselves#✓fully proved

Let \(v\) and \(t\) be terms of the same type in the same context. If \(v\) is a value and \(v\) reduces to \(t\) in zero or more call-by-value steps, then \(v = t\).

theorem eq_of_value_source {v t : Tm Γ A} (hv : Value v) (h : Steps v t) : v = t

Uses 6 · Used by 1

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesSmall-step call-by-value reduction in STLC · Values are irreducible

Used byUniqueness of the value reached by evaluation

TheoremUniqueness of the value reached by evaluation#✓fully proved

Let \(t\) be a term in any context. If \(t\) reduces in zero or more call-by-value steps to a value \(v\) and also to a value \(w\), then \(v = w\).

theorem value_unique {t v w : Tm Γ A} (htv : Steps t v) (hv : Value v)
    (htw : Steps t w) (hw : Value w) : v = w

Uses 6 · Used by 3

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesValues reduce only to themselves · Evaluation to a value passes through every reduct

Used byUniqueness of normal forms · Transitivity of having the same result · Determinism of big-step evaluation in the simply typed lambda calculus

DefinitionNormalizing closed terms#✓fully proved

A closed term \(t\) of the simply typed lambda calculus normalizes when it reduces, in zero or more call-by-value steps, to a term in normal form, that is, a term with no further call-by-value reduction step.

def Normalizes (t : Tm [] A) : Prop := ∃ n, Steps t n ∧ Step.NormalForm n

Uses 4 · Used by 2

Statement usesNormal forms for call-by-value reduction in STLC · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Used byNormalization and termination coincide · Normalization of closed terms

TheoremNormalization and termination coincide#✓fully proved

A closed well-typed term \(t\) normalizes, that is, reduces in zero or more call-by-value steps to a normal form (a term with no further reduction step), if and only if it terminates, that is, reduces in zero or more call-by-value steps to a value.

theorem iff_terminates {t : Tm [] A} : Normalizes t ↔ Terminates t

Uses 8 · Used by 1

Statement usesNormalizing closed terms · Termination of closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesNormal forms for call-by-value reduction in STLC · Closed normal forms are exactly the values · Multi-step call-by-value reduction in STLC · Values of STLC

Used byNormalization of closed terms

TheoremNormalization of closed terms#✓fully proved

Every closed well-typed term normalizes: it reduces in zero or more call-by-value steps to a normal form.

theorem normalizes_closed (t : Tm [] A) : Normalizes t

Uses 6

Statement usesNormalizing closed terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesNormalization and termination coincide · Termination of closed terms · Termination of the call-by-value simply typed lambda calculus

TheoremUniqueness of normal forms#✓fully proved

If a closed term \(t\) reduces in zero or more call-by-value steps to a normal form \(n\) and also to a normal form \(m\), then \(n = m\).

theorem normalForm_unique {t n m : Tm [] A} (htn : Steps t n) (hn : Step.NormalForm n)
    (htm : Steps t m) (hm : Step.NormalForm m) : n = m

Uses 7

Statement usesNormal forms for call-by-value reduction in STLC · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesClosed normal forms are exactly the values · Uniqueness of the value reached by evaluation · Values of STLC

TheoremClosed functions evaluate to lambda abstractions#✓fully proved

For every closed term \(f\) of a function type \(A \Rightarrow B\) there is a term \(b\) of type \(B\) in the context with a single variable of type \(A\) such that \(f\) reduces, in zero or more call-by-value steps, to the lambda abstraction with body \(b\).

theorem closed_function_evaluates_to_lam (f : Tm [] (A ⇒ B)) :
    ∃ body : Tm [A] B, Steps f (.lam body)

Uses 7

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesCanonical forms for closed function values · Termination of closed terms · Values of STLC · Termination of the call-by-value simply typed lambda calculus

TheoremNo closed terms of base type#✓fully proved

In the pure, constant-free calculus there is no closed term whose type is a base type.

theorem no_closed_base (b : Base) (t : Tm [] (.base b)) : False

Uses 6

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesMulti-step call-by-value reduction in STLC · Termination of closed terms · Values of STLC · Termination of the call-by-value simply typed lambda calculus

DefinitionClosed terms with the same result#✓fully proved

Two closed terms \(t\) and \(u\) of the same type have the same result when there is a value \(v\) such that both \(t\) and \(u\) reduce to \(v\) in zero or more call-by-value steps.

def SameResult (t u : Tm [] A) : Prop :=
  ∃ v, Steps t v ∧ Steps u v ∧ Value v

Uses 4 · Used by 8

Statement usesMulti-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Used byLeft expansion preserves having the same result · Right expansion preserves having the same result · Application preserves having the same result · Evaluation preserves the result of a closed term · Reflexivity of having the same result · Having the same result is an equivalence relation · Symmetry of having the same result · Transitivity of having the same result

TheoremReflexivity of having the same result#✓fully proved

Every closed term has the same result as itself.

theorem refl (t : Tm [] A) : SameResult t t

Uses 7 · Used by 1

Statement usesClosed terms with the same result · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesMulti-step call-by-value reduction in STLC · Termination of closed terms · Values of STLC · Termination of the call-by-value simply typed lambda calculus

Used byHaving the same result is an equivalence relation

TheoremSymmetry of having the same result#✓fully proved

If closed terms \(t\) and \(u\) have the same result, then \(u\) and \(t\) have the same result.

theorem symm {t u : Tm [] A} (h : SameResult t u) : SameResult u t

Uses 5 · Used by 2

Statement usesClosed terms with the same result · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesMulti-step call-by-value reduction in STLC · Values of STLC

Used byRight expansion preserves having the same result · Having the same result is an equivalence relation

TheoremTransitivity of having the same result#✓fully proved

If closed terms \(t\) and \(u\) have the same result, and \(u\) and a closed term \(v\) have the same result, then \(t\) and \(v\) have the same result.

theorem trans {t u v : Tm [] A} (htu : SameResult t u) (huv : SameResult u v) :
    SameResult t v

Uses 6 · Used by 3

Statement usesClosed terms with the same result · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesMulti-step call-by-value reduction in STLC · Uniqueness of the value reached by evaluation · Values of STLC

Used byLeft expansion preserves having the same result · Right expansion preserves having the same result · Having the same result is an equivalence relation

TheoremEvaluation preserves the result of a closed term#✓fully proved

If a closed term \(t\) reduces to a term \(u\) in zero or more call-by-value steps, then \(t\) and \(u\) have the same result.

theorem of_steps {t u : Tm [] A} (htu : Steps t u) : SameResult t u

Uses 8 · Used by 2

Statement usesClosed terms with the same result · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSmall-step call-by-value reduction in STLC · Termination of closed terms · Values of STLC · Termination of the call-by-value simply typed lambda calculus

Used byLeft expansion preserves having the same result · Right expansion preserves having the same result

TheoremLeft expansion preserves having the same result#✓fully proved

Let \(t\), \(t'\) and \(u\) be closed terms of the same type. If \(t\) reduces to \(t'\) in zero or more call-by-value steps, and \(t'\) and \(u\) have the same result, then \(t\) and \(u\) have the same result.

theorem anti_left {t t' u : Tm [] A} (htt' : Steps t t') (h : SameResult t' u) :
    SameResult t u

Uses 6

Statement usesClosed terms with the same result · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesEvaluation preserves the result of a closed term · Transitivity of having the same result

TheoremRight expansion preserves having the same result#✓fully proved

Let \(t\), \(u\) and \(u'\) be closed terms of the same type. If \(u\) reduces to \(u'\) in zero or more call-by-value steps, and \(t\) and \(u'\) have the same result, then \(t\) and \(u\) have the same result.

theorem anti_right {t u u' : Tm [] A} (huu' : Steps u u') (h : SameResult t u') :
    SameResult t u

Uses 7

Statement usesClosed terms with the same result · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesEvaluation preserves the result of a closed term · Symmetry of having the same result · Transitivity of having the same result

TheoremApplication preserves having the same result#✓fully proved

Let \(f\) and \(g\) be closed terms of a function type \(A \Rightarrow B\), and let \(a\) and \(b\) be closed terms of type \(A\). If \(f\) and \(g\) have the same result and \(a\) and \(b\) have the same result, then the applications \(f\,a\) and \(g\,b\) have the same result.

theorem app {f g : Tm [] (A ⇒ B)} {a b : Tm [] A}
    (hfg : SameResult f g) (hab : SameResult a b) :
    SameResult (.app f a) (.app g b)

Uses 12

Statement usesClosed terms with the same result · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSmall-step call-by-value reduction in STLC · Canonical forms for closed function values · Multi-step call-by-value reduction in STLC · Evaluating the argument of a value function is a multi-step congruence · Multi-step evaluation is a congruence in function position · Termination of closed terms · Instantiating a binder body (simply typed lambda calculus) · Values of STLC · Termination of the call-by-value simply typed lambda calculus

TheoremHaving the same result is an equivalence relation#✓fully proved

For every simple type \(A\), the relation of having the same result is an equivalence relation on the closed terms of type \(A\).

theorem sameResult_equivalence : Equivalence (@SameResult Base A)

Uses 6

Statement usesClosed terms with the same result · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesReflexivity of having the same result · Symmetry of having the same result · Transitivity of having the same result

35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.