∀ h k n1 n2 p1 p2 f1 f2, n1 = O ⇒ sub_hk h k n1 n2 p1 p2 f1 f2

Theorem sub_hkO : forall (h:(nat.nat -> nat.nat)), forall (k:(nat.nat -> nat.nat)), forall (n1:nat.nat), forall (n2:nat.nat), forall (p1:(nat.nat -> bool.bool)), forall (p2:(nat.nat -> bool.bool)), forall (f1:(nat.nat -> nat.nat)), forall (f2:(nat.nat -> nat.nat)), (logic.eq (nat.nat) n1 nat.O) -> sub_hk h k n1 n2 p1 p2 f1 f2.

theorem sub_hkO : \forall (h:nat -> nat). \forall (k:nat -> nat). \forall (n1:nat). \forall (n2:nat). \forall (p1:nat -> bool). \forall (p2:nat -> bool). \forall (f1:nat -> nat). \forall (f2:nat -> nat). ((eq) (nat) n1 (O) ) -> (sub_hk) h k n1 n2 p1 p2 f1 f2.

theorem sub_hkO : forall (h:(nat.nat) -> nat.nat) , forall (k:(nat.nat) -> nat.nat) , forall (n1:nat.nat) , forall (n2:nat.nat) , forall (p1:(nat.nat) -> bool.bool) , forall (p2:(nat.nat) -> bool.bool) , forall (f1:(nat.nat) -> nat.nat) , forall (f2:(nat.nat) -> nat.nat) , ((((logic.eq_) (nat.nat)) (n1)) ((nat.O) )) -> (((((((((bigops.sub_hk) ) (h)) (k)) (n1)) (n2)) (p1)) (p2)) (f1)) (f2).

sub_hkO : LEMMA (FORALL(h:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(k:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n1:nat_sttfa_th.sttfa_nat):(FORALL(n2:nat_sttfa_th.sttfa_nat):(FORALL(p1:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(p2:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(f2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n1)(nat_sttfa_th.sttfa_O) => bigops_sttfa.sub_hk(h)(k)(n1)(n2)(p1)(p2)(f1)(f2))))))))))

Printing for OpenTheory is not working at the moment.