happy-tope-nested-rec-or-d6.rzk

#lang rzk-1

-- Full binary nested `recOR` over 6 shaped coordinates (see `happy-tope-nested-rec-or.rzk`).

#define u : U := Unit

-- coordinate t0
-- coordinate t1
-- coordinate t2
-- coordinate t3
-- coordinate t4
-- coordinate t5

#define nest (t0 : 2 | (t0 === 0_2) \/ (t0 === 1_2)) (t1 : 2 | (t1 === 0_2) \/ (t1 === 1_2)) (t2 : 2 | (t2 === 0_2) \/ (t2 === 1_2)) (t3 : 2 | (t3 === 0_2) \/ (t3 === 1_2)) (t4 : 2 | (t4 === 0_2) \/ (t4 === 1_2)) (t5 : 2 | (t5 === 0_2) \/ (t5 === 1_2)) : U
  := recOR( t0 === 0_2 |-> recOR( t1 === 0_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ) ), t1 === 1_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ) ) ), t0 === 1_2 |-> recOR( t1 === 0_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ) ), t1 === 1_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ), t3 === 1_2 |-> recOR( t4 === 0_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ), t4 === 1_2 |-> recOR( t5 === 0_2 |-> u, t5 === 1_2 |-> u ) ) ) ) ) )