mod! OTSLOGIC {
 op ~_ : Bool -> Bool {prec: 53}
 op _/\_ : Bool Bool -> Bool {comm assoc prec: 55 r-assoc}
 op _\/_ : Bool Bool -> Bool {comm assoc prec: 59 r-assoc}
 op _=>_ : Bool Bool -> Bool {prec: 61 r-assoc}
 op _<=>_ : Bool Bool -> Bool {comm prec: 63 r-assoc}
 op eval : Bool -> Bool
 op invariant_ : Bool -> Bool
 op _ensures_ : Bool Bool -> Bool
 op _|-->_ : Bool Bool -> Bool
-- CafeOBJ variables
 vars P Q R P1 Q1 R1 R2 : Bool
-- equations
 ceq (invariant (P1 => Q1)) => (P |--> Q) = true 
     if eval(P => P1) and eval(Q1 => Q) .
 ceq ((P1 ensures Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(Q1 => Q) .
 ceq ((P1 |--> Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(Q1 => Q) .
 --
 ceq ((P1 |--> R /\ R1 |--> Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq ((P1 ensures R /\ R1 ensures Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq (((invariant (P1 => R)) /\ (invariant (R1 => Q1))) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq ((P1 |--> R /\ R1 ensures Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq ((P1 |--> R /\ (invariant (R1 => Q1))) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq ((P1 ensures R /\ R1 |--> Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq ((P1 ensures R /\ (invariant (R1 => Q1))) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq (((invariant (P1 => R)) /\ R1 |--> Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 ceq (((invariant (P1 => R)) /\ R1 ensures Q1) => (P |--> Q)) = true 
     if eval(P => P1) and eval(R => R1) and eval(Q1 => Q) .
 --
 ceq ((P1 |--> R1 /\ Q1 |--> R2) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq ((P1 ensures R1 /\ Q1 ensures R2) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq (((invariant (P1 => R1)) /\ (invariant (Q1 => R2))) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq ((P1 |--> R1 /\ Q1 ensures R2) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq ((P1 |--> R1 /\ (invariant (Q1 => R2))) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq ((P1 ensures R1 /\ Q1 |--> R2) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq ((P1 ensures R1 /\ (invariant (Q1 => R2))) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq (((invariant (P1 => R1)) /\ Q1 |--> R2) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 ceq (((invariant (P1 => R1)) /\ Q1 ensures R2) => (P |--> R)) = true 
     if eval(P => (P1 \/ Q1)) and eval(R1 <=> R2) and eval(R1 => R) .
 --
 eq eval(true) = true .
 eq eval(false) = false .
 eq eval(~ P) = not eval(P) .
 eq eval(P /\ Q) = eval(P) and eval(Q) .
 eq eval(P \/ Q) = eval(P) or eval(Q) .
 eq eval(P => Q) = eval(P) implies eval(Q) .
 eq eval(P <=> Q) = eval(P) iff eval(Q) .
}

mod* EQLTRIV {
  [Elt]
  op _<_ : Elt Elt -> Bool -- well-founded relaton on Elt
  op _=_ : Elt Elt -> Bool {comm}
}

mod! INDUCTIONOFLEADSTO(D :: EQLTRIV) {
  pr(OTSLOGIC)
-- CafeOBJ variables
  vars P Q P1 Q1 : Bool
  vars M X : Elt.D
-- equations
  ceq ((P1 /\ (M = X)) |--> ((P1 /\ (M < X)) \/ Q1)) => (P |--> Q) = true 
      if eval(P => P1) and eval(Q1 => Q) .
}