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

#lang rzk-1

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

#define u : U := Unit

-- coordinate t0
-- coordinate t1
-- coordinate t2
-- coordinate t3

#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)) : U
  := recOR( t0 === 0_2 |-> recOR( t1 === 0_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ) ), t1 === 1_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ) ) ), t0 === 1_2 |-> recOR( t1 === 0_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ) ), t1 === 1_2 |-> recOR( t2 === 0_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ), t2 === 1_2 |-> recOR( t3 === 0_2 |-> u, t3 === 1_2 |-> u ) ) ) )