<commit_before>------------------------------------------------------------------------------
-- Equations for the division
------------------------------------------------------------------------------

module Examples.Division.EquationsER where

open import LTC.Minimal
open import LTC.MinimalER

open import Examples.Division
open import LTC.Function.ArithmeticPCF
open import LTC.Relation.Equalities.PropertiesER
open import LTC.Relation.InequalitiesPCF

import MyStdLib.Relation.Binary.EqReasoning
open module APER = MyStdLib.Relation.Binary.EqReasoning.StdLib _≡_ refl trans

------------------------------------------------------------------------------
-- Division properties

private
    -- Before to prove some properties for 'div i j' it is convenient
    -- to have a proof for each possible execution step.

    -- Initially, we define the possible states ('div-s₁',
    -- 'dih-s₂', ...) and after that, we write down the proof for
    -- the execution step from the state 'p' to the state 'q'
    -- (i.e. (i j : D) → div-sp i j → div-sq i j).

    -- Initially, 'cFix' conversion rule is applied
    div-s₁ : D → D → D
    div-s₁ i j = divh (fix divh) ∙ i ∙ j

    -- First argument application
    div-s₂ : D → D → D
    div-s₂ i j = fun ∙ j<commit_msg>Added doc.<commit_after>------------------------------------------------------------------------------
-- Equations for the division
------------------------------------------------------------------------------

module Examples.Division.EquationsER where

open import LTC.Minimal
open import LTC.MinimalER

open import Examples.Division
open import LTC.Function.ArithmeticPCF
open import LTC.Relation.Equalities.PropertiesER
open import LTC.Relation.InequalitiesPCF

import MyStdLib.Relation.Binary.EqReasoning
open module APER = MyStdLib.Relation.Binary.EqReasoning.StdLib _≡_ refl trans

------------------------------------------------------------------------------
-- Division properties

-- Note: This module was written for the version of div using the
-- lambda abstractions, but we can use it with the version of div
-- using super-combinators.

private
    -- Before to prove some properties for 'div i j' it is convenient
    -- to have a proof for each possible execution step.

    -- Initially, we define the possible states ('div-s₁',
    -- 'dih-s₂', ...) and after that, we write down the proof for
    -- the execution step from the state 'p' to the state 'q'
    -- (i.e. (i j : D) → div-sp i j → div-sq i j).

    -- Initially, 'cFix' conversion rule is applied
    div-s₁ : D → D → D
    div-s₁ i j = divh (fix divh) ∙ i ∙ j

    -- First argument application
    div-s₂ : D → D → D
    div-s₂ i j = fun ∙ j
{'fraction_non_alphanumeric': 0.25018532246108227, 'fraction_numerical': 0.0, 'mean_word_length': 1.5976900866217516, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6119863', 'n_tokens_mistral': 736, 'n_tokens_neox': 730, 'n_words': 298}