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 (∅g ↦g s ↦g t)
fill⇔ instantiate f s = instantiate f t
fill∧ elaborate' f (Unit ∅g ↦g s ↦g t)
fill⇔ instantiate f s ∈g instantiate f t
fill∧ elaborate'
fillf
fill(Pairg (Unit ∅g) ∅g
fill↦g v
fill↦g s
fill↦g 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