∀ h k n1 n2 p1 p2 f1 f2, n1 = O ⇒ sub_hk h k n2 n1 p2 p1 f2 f1 ⇒ ∀ i, i < n2 ⇒ (p2 i) = false

Theorem sub0_to_false : 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 n2 n1 p2 p1 f2 f1) -> forall (i:nat.nat), (nat.lt i n2) -> logic.eq (bool.bool) (p2 i) bool.false.

theorem sub0_to_false : \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 n2 n1 p2 p1 f2 f1) -> \forall (i:nat). ((lt) i n2) -> (eq) (bool) (p2 i) (false) .

theorem sub0_to_false : 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)) (n2)) (n1)) (p2)) (p1)) (f2)) (f1)) -> forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n2)) -> (((logic.eq_) (bool.bool)) ((p2) (i))) ((bool.false) ).

sub0_to_false : 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)(n2)(n1)(p2)(p1)(f2)(f1) => (FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n2) => logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p2(i))(bool_sttfa_th.sttfa_false)))))))))))))

Printing for OpenTheory is not working at the moment.