def KnowledgeFn (World Ent : Type u) (n : ℕ) : Type u

Equations

• KnowledgeFn World Ent 0 = PUnit.{?u.1 + 1}
• KnowledgeFn World Ent n_2.succ = (Ent → World → KnowledgeFn World Ent n_2 → Prop)

structure Knowledge (World Ent : Type u) : Type u

• depth : ℕ
• fn : KnowledgeFn World Ent self.depth

structure WorldWithKnowledge (World Ent : Type u) : Type u

• world : World
• knowledge : Knowledge World Ent

def KnowledgeFnWf {World Ent : Type u} (w : World) (n : ℕ) (f : KnowledgeFn World Ent n) : Prop

Equations

• KnowledgeFnWf w 0 x = True
• KnowledgeFnWf w n_2.succ p = ∀ (e : Ent), ∃ (f' : KnowledgeFn World Ent n_2), KnowledgeFnWf w n_2 f' ∧ p e w f'

def Knowledge.WF {World Ent : Type u} (k : Knowledge World Ent) (w : World) : Prop

Equations

• k.WF w = KnowledgeFnWf w k.depth k.fn

def Knowledge.SatisfiesAnyW {World Ent : Type u} (k : Knowledge World Ent) (e : Ent) (w : World) : Prop

Equations

• k.SatisfiesAnyW e w = match k.depth, k.fn with | 0, x => True | n.succ, p => ∃ (f' : KnowledgeFn World Ent n), p e w f'

def Knowledge.SatisfiesAllW {World Ent : Type u} (k : Knowledge World Ent) (e : Ent) (w : World) : Prop

Equations

• k.SatisfiesAllW e w = match k.depth, k.fn with | 0, x => True | n.succ, p => ∀ (f' : KnowledgeFn World Ent n), p e w f'

def WorldWithKnowledge.WF {World Ent : Type u} (wk : WorldWithKnowledge World Ent) : Prop

Equations

• wk.WF = wk.knowledge.WF wk.world

def Knowledge.KnowsW {World Ent : Type u} (k : Knowledge World Ent) (e : Ent) (p : World → Prop) (w : World) : Prop

Equations

• k.KnowsW e p w = (p w ∧ ∀ (w' : World), k.SatisfiesAnyW e w' → p w')

def WorldWithKnowledge.KnowsW {World Ent : Type u} (wk : WorldWithKnowledge World Ent) (e : Ent) (p : World → Prop) : Prop

Equations

• wk.KnowsW e p = wk.knowledge.KnowsW e p wk.world