The Theory refl-defs
Parents
gst
Constants
instantiate
(GS → GS) → GS → GS
$∈gp
GS → GS → BOOL
$p
GS → GS → GS
elaborate
(GS → GS) → GS → BOOL
$∈gd
GS → GS → BOOL
Fixity
Right Infix 230:
gd gp
Right Infix 240:
p
Definitions
instantiate
⊢ ConstSpec
fill(λ instantiate'
fill• ∀ f s
fill• instantiate' f (Unit s)
fill= Imagep (instantiate' f) s
fill∧ (¬ (∃ t• s = Unit t)
fill⇒ instantiate' f s = f s))
fillinstantiate
gp
⊢ ∀ s t• s ∈gp t ⇔ (∃ f• s = instantiate f t)
p
⊢ ∀ f x• f p x = (ε y• x ↦g y ∈gp f)
elaborate
⊢ ConstSpec
fill(λ elaborate'
fill• ∀ f s t v
fill• elaborate' f (∅gg s ↦g t)
fill⇔ instantiate f s = instantiate f t
fill∧ elaborate' f (Unit ∅gg s ↦g t)
fill⇔ instantiate f s ∈g instantiate f t
fill∧ elaborate'
fillf
fill(Pairg (Unit ∅g) ∅g
fillg v
fillg s
fillg t)
fill⇔ ¬ (∀ x
fill• (let f' y = (if y = v then x else f y)
fillin elaborate' f' s
fill∧ elaborate' f' t)))
fillelaborate
gd
⊢ ∀ s t• s ∈gd t ⇔ elaborate (λ v• s) t

up quick index

privacy policy

Created:

V