liamoc.net
my forest
1\date{2025-12-03T06:15:34Z}
2\author{liamoc}
3\taxon{Example}
4\import{shiki-macros}
5\put\shiki/language{Isabelle Theory}
6\title{Wellformedness for \code{oots}}
7\p{We define \code{well}, an inductive wellformedness predicate for \code{oots} sequences, that state there are no segments of zero length, and that no two adjacent segments have the same \code{oot} value.}
8\shiki{inductive well :: ‹oots ⇒ bool› where
9 ‹well Empty›
10| ‹n > 0 ⟹ well (ONEs n Empty)›
11| ‹n > 0 ⟹ well (TWOs n Empty)›
12| ‹n > 0 ⟹ well (ONEs m r) ⟹ well (TWOs n (ONEs m r))›
13| ‹n > 0 ⟹ well (TWOs m r) ⟹ well (ONEs n (TWOs m r))›}