Library hydras.Epsilon0.Large_Sets_Examples

From hydras Require Import E0 Canon Paths MoreLists Large_Sets.


Example ex_pathS1 : pathS T1omega (2::3::4::nil) 1.

Example ex_pathS2 : pathS T1omega (interval 3 6) 1.

Example omega_omega_1_4 : gnaw (T1omega ^ T1omega) (interval 1 4) = 0.

Example omega_omega_1_3 : gnaw (T1omega ^ T1omega) (interval 1 3) = 1.

Inductive answer : Set := Ok | Too_far | Remaining (rest : ppT1).

Definition large_set_check alpha i j :=
  let beta := gnaw alpha (interval i (Nat.pred j))
  in match beta with
     | one ⇒ Ok
     | zero ⇒ Too_far
     | _ ⇒ Remaining (pp (canon beta j))
     end.








#[global] Hint Resolve iota_from_lt_not_In: core.

Example Ex1 : mlarge (T1omega × T1omega) (interval 6 510).

Example Ex2 : large (T1omega × T1omega) (interval 6 700).