(* Inductively defined relations on nat x word. *) Module indrel Import lib_nat word ; [ Rel = nat->word->Prop ]; [ OpRel = Rel -> Rel ]; [ Contain = [O,P:Rel] {n:nat}{w:word}(O n w)-> P n w ]; Goal {O:Rel} Contain O O; Intros O n w o ; Immed ; Save Contain_refl ; Goal {O,P,Q:Rel} (Contain O P) -> (Contain P Q) -> Contain O Q; Intros O P Q op pq n w onw ; Refine pq ; Refine op ; Immed ; Save Contain_trans ; [ Monotone = [o : OpRel] {O,P:Rel} (Contain O P) -> Contain (o O) (o P) ]; [ Fix = [o : OpRel] [n:nat][w:word] {O : Rel} (Contain (o O) O) -> O n w ]; [ o : OpRel] [m : Monotone o]; Goal {O:Rel} (Contain (o O) O) -> Contain (Fix o) O; Intros O coOO n w fwn ; Refine fwn ; Immed; Save Fix_lower_lemma ; Goal Contain (o (Fix o)) (Fix o); Intros n w oFo P pFpP ; Refine pFpP ; Refine m (Fix o) P; Refine Fix_lower_lemma ; Immed ; Save Fix_contracts ; Goal Contain (Fix o) (o (Fix o)); Refine Fix_lower_lemma ; Refine m; Refine Fix_contracts; Save Fix_expands ; Discharge o;