{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Algorithmic.Properties where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Algorithmic
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils

-- Algorithmic.Properties.lem-·⋆
d_lem'45''183''8902'_28 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lem'45''183''8902'_28 :: T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T_Σ_14
d_lem'45''183''8902'_28 ~T_Kind_476
v0 ~T_Kind_476
v1 ~T__'8866'Nf'8902'__4
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8866'Nf'8902'__4
v5 ~T__'8866'__168
v6 ~T__'8866'__168
v7 ~T__'8866'Nf'8902'__4
v8 ~T__'8801'__12
v9
                        ~T__'8801'__12
v10 ~T__'8801'__12
v11
  = T_Σ_14
du_lem'45''183''8902'_28
du_lem'45''183''8902'_28 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lem'45''183''8902'_28 :: T_Σ_14
du_lem'45''183''8902'_28
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
         ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased))
-- Algorithmic.Properties.lem-unwrap
d_lem'45'unwrap_54 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lem'45'unwrap_54 :: T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T_Σ_14
d_lem'45'unwrap_54 ~T_Kind_476
v0 ~T_Kind_476
v1 ~T__'8866'Nf'8902'__4
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8866'Nf'8902'__4
v5 ~T__'8866'__168
v6 ~T__'8866'__168
v7 ~T__'8866'Nf'8902'__4
v8 ~T__'8801'__12
v9 ~T__'8801'__12
v10
                   ~T__'8801'__12
v11
  = T_Σ_14
du_lem'45'unwrap_54
du_lem'45'unwrap_54 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lem'45'unwrap_54 :: T_Σ_14
du_lem'45'unwrap_54
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased
         ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased))