(* ---------------------------------------------------------- *)
(* --- Axiomatic 'IterAxioms'                             --- *)
(* ---------------------------------------------------------- *)

Require Import ZArith.
Require Import Reals.
Require Import BuiltIn.
Require Import int.Int.
Require Import int.Abs.
Require Import int.ComputerDivision.
Require Import real.Real.
Require Import real.RealInfix.
Require Import real.FromInt.
Require Import map.Map.
Require Import Qedlib.
Require Import Qed.
Require Import S1__Iter.

Parameter L_inc : S1__Iter -> S1__Iter.

Parameter P_eq : S1__Iter -> S1__Iter -> Prop.

Hypothesis Q_TL_inc: forall (I : S1__Iter), ((IsS1__Iter I)) ->
  ((IsS1__Iter ((L_inc I)))).

Hypothesis Q_eqRefl: forall (I : S1__Iter), ((IsS1__Iter I)) -> ((P_eq I I)).

Hypothesis Q_eqSym: forall (I_1 I : S1__Iter), ((IsS1__Iter I)) ->
  ((IsS1__Iter I_1)) -> ((P_eq I_1 I)) -> ((P_eq I I_1)).

Hypothesis Q_eqTrns: forall (I_2 I_1 I : S1__Iter), ((IsS1__Iter I)) ->
  ((IsS1__Iter I_1)) -> ((IsS1__Iter I_2)) -> ((P_eq I_1 I)) ->
  ((P_eq I_2 I_1)) -> ((P_eq I_2 I)).