Obs.notations

Obs.list_tools

• RIS.list tools : Toolbox of list operators and their properties.
• Lists
  • Notations
  • Induction principles
  • General lemmas
  • Lists of pairs
  • Lists as finite sets
  • More general lemmas
  • Subsets of a list
  • Pairs
  • Enumerate lists of a certain length
  • Pad a list with an element
• Sum function
• Enumerate permutations of a list

Obs.decidable_prop

• Decidable sets

Obs.list_dec

• Lists over a decidable set

Obs.coherence_graph

• Main definitions
• Decidable Graphs
• Finite cliques

Obs.syntax_obs

• Syntax for observations

Obs.equiv_obs

• Axiomatic equivalence of observations

Obs.laws

• Useful laws of Heyting algebras
• Basic laws
• inf_obs A⁺ is a partial order with respect to equiv_Obs
• Lattice properties
• Properties of the implication
• Additional laws
• n-ary meets and joins
• Finite and singleton cliques

Obs.sem_obs

• Semantics of observation terms

Obs.fan

• Graphs with finite anti-neighbourhoods.

Obs.anticlique

• Anticlique graph : an infinite graph with no edge
• Definition of the graph
• Axiomatisation
• Basic laws
• Representations
• Cliques are either empty or singletons
• Isomorphism between cliques and option V
• The axioms are sound
• From representations to terms
• From terms to reprentations
• Main results

Obs.product

Obs.fin_sem_obs