gistfile1.txt

  Theorem iter_fin {A: Type} (k: nat) (O: (A -> bool) -> (A -> bool)) :
    mon O -> bounded_card A k ->
    forall n: nat, forall a: A, iter O n nil_pred a = true -> iter O k nil_pred a = true.
  Proof. 
  intros Hmon Hboun; unfold bounded_card in Hboun.
  destruct Hboun as [l [Hin Hlen]]. intros n.
  assert (Hle : k < n \/ k >= n) by omega.    
  destruct Hle as [Hlel | Hler]; swap 1 2.
  destruct (iter_aux_newagain O l Hmon Hin k). intros a Hiter.
  specialize (increasing O Hmon); intros. unfold pred_subset in H0.
  (* induction on Hler *)
  induction Hler. assumption.
  replace (S m) with (plus m 1); swap 1 2. omega.
  apply H0. specialize (H0 m).


 
  A : Type
  O : (A -> bool) -> A -> bool
  Hmon : mon O
  l : list A
  Hin : forall a : A, In a l
  m : nat
  Hlen : length l <= S m
  n : nat
  Hler : n <= m
  H : forall a : A, iter O (S m) nil_pred a = true <-> iter O (S m + 1) nil_pred a = true
  a : A
  Hiter : iter O n nil_pred a = true
  H0 : forall a : A, iter O m nil_pred a = true -> iter O (m + 1) nil_pred a = true
  IHHler : length l <= m ->
           (forall a : A, iter O m nil_pred a = true <-> iter O (m + 1) nil_pred a = true) ->
           iter O m nil_pred a = true
  ============================
  iter O m nil_pred a = true
  
  
  

A : Type
k : nat
O : (A -> bool) -> A -> bool
Hmon : mon O
l : list A
Hin : forall a : A, In a l
Hlen : length l <= k
a : A
m : nat
H : iter O (S m) nil_pred a = true
Hl : forall a : A, iter O k nil_pred a = true <-> iter O (k + 1) nil_pred a = true
Hlel : S k <= m
IHHlel : iter O m nil_pred a = true -> iter O k nil_pred a = true

iter O k nil_pred a = true

subgoal 2 (ID 387) is:
iter O k nil_pred a = true