Let X, Tx, U0, x0 and An be given.
Assume Hcomp: compact_space X Tx.
Assume HH: Hausdorff_space X Tx.
Assume HAn: ∀n : set, n ∈ ω → closed_in X Tx (An n) ∧ interior_of X Tx (An n) = Empty.
Assume HU0: U0 ∈ Tx.
Assume Hx0X: x0 ∈ X.
Assume Hx0U0: x0 ∈ U0.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim Hnorm: normal_space X Tx.
An exact proof term for the current goal is (compact_Hausdorff_normal X Tx Hcomp HH).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (normal_space_implies_regular X Tx Hnorm).
Set BaseState to be the term (x0,U0).
Set xcur to be the term (λst : set ⇒ st 0).
Set Bcur to be the term (λst : set ⇒ st 1).
Set StepState to be the term (λn st : set ⇒ Eps_i (λt : set ⇒ ∃x1 : set, ∃B1 : set, t = (x1,B1) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n)))))).
Set State to be the term (λn : set ⇒ nat_primrec BaseState StepState n).
Set xn to be the term (λn : set ⇒ xcur (State n)).
Set Bn to be the term (λn : set ⇒ Bcur (State n)).
We prove the intermediate claim HBase_x: xn 0 = x0.
We prove the intermediate claim HSt0: State 0 = BaseState.
We prove the intermediate claim Hdef: State 0 = nat_primrec BaseState StepState 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (nat_primrec_0 BaseState StepState).
We prove the intermediate claim Hxn0: xn 0 = xcur (State 0).
Use reflexivity.
rewrite the current goal using Hxn0 (from left to right).
rewrite the current goal using HSt0 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq x0 U0).
We prove the intermediate claim HBase_B: Bn 0 = U0.
We prove the intermediate claim HSt0: State 0 = BaseState.
We prove the intermediate claim Hdef: State 0 = nat_primrec BaseState StepState 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (nat_primrec_0 BaseState StepState).
We prove the intermediate claim HBn0: Bn 0 = Bcur (State 0).
Use reflexivity.
rewrite the current goal using HBn0 (from left to right).
rewrite the current goal using HSt0 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq x0 U0).
We prove the intermediate claim HStepState_ax: ∀n st : set, (∃t : set, ∃x1 : set, ∃B1 : set, t = (x1,B1) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n))))) → ∃x1 : set, ∃B1 : set, StepState n st = (x1,B1) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n)))).
Let n and st be given.
Assume Hex: ∃t : set, ∃x1 : set, ∃B1 : set, t = (x1,B1) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n)))).
Set P to be the term (λt : set ⇒ ∃x1 : set, ∃B1 : set, t = (x1,B1) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n))))).
We prove the intermediate claim HexP: ∃t : set, P t.
An exact proof term for the current goal is Hex.
We prove the intermediate claim HP: P (Eps_i P).
An exact proof term for the current goal is (Eps_i_ex P HexP).
We prove the intermediate claim Hdef: StepState n st = Eps_i P.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is HP.
Set Inv to be the term (λn : set ⇒ xn n ∈ X ∧ Bn n ∈ Tx ∧ xn n ∈ Bn n).
We prove the intermediate claim HInv0: Inv 0.
We prove the intermediate claim HInv0def: Inv 0 = (xn 0 ∈ X ∧ Bn 0 ∈ Tx ∧ xn 0 ∈ Bn 0).
Use reflexivity.
rewrite the current goal using HInv0def (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
rewrite the current goal using HBase_x (from left to right).
An exact proof term for the current goal is Hx0X.
rewrite the current goal using HBase_B (from left to right).
An exact proof term for the current goal is HU0.
rewrite the current goal using HBase_x (from left to right).
rewrite the current goal using HBase_B (from left to right).
An exact proof term for the current goal is Hx0U0.
We prove the intermediate claim HState_succ: ∀n : set, nat_p n → State (ordsucc n) = StepState n (State n).
Let n be given.
Assume HnNat: nat_p n.
We prove the intermediate claim HdefL: State (ordsucc n) = nat_primrec BaseState StepState (ordsucc n).
Use reflexivity.
We prove the intermediate claim HdefR: State n = nat_primrec BaseState StepState n.
Use reflexivity.
rewrite the current goal using HdefL (from left to right).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is (nat_primrec_S BaseState StepState n HnNat).
We prove the intermediate claim HInvStep: ∀n : set, nat_p n → Inv n → Inv (ordsucc n).
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
We prove the intermediate claim HInvnEq: Inv n = (xn n ∈ X ∧ Bn n ∈ Tx ∧ xn n ∈ Bn n).
Use reflexivity.
We prove the intermediate claim HInvn': xn n ∈ X ∧ Bn n ∈ Tx ∧ xn n ∈ Bn n.
rewrite the current goal using HInvnEq (from right to left).
An exact proof term for the current goal is HInvn.
Apply HInvn' to the current goal.
Assume Hpair HxBn.
Apply Hpair to the current goal.
Assume HxX HBnTx.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
We prove the intermediate claim HAnPack: closed_in X Tx (An n) ∧ interior_of X Tx (An n) = Empty.
An exact proof term for the current goal is (HAn n HnO).
We prove the intermediate claim HAcl: closed_in X Tx (An n).
An exact proof term for the current goal is (andEL (closed_in X Tx (An n)) (interior_of X Tx (An n) = Empty) HAnPack).
We prove the intermediate claim HAint: interior_of X Tx (An n) = Empty.
An exact proof term for the current goal is (andER (closed_in X Tx (An n)) (interior_of X Tx (An n) = Empty) HAnPack).
We prove the intermediate claim HexStep: ∃x1 : set, ∃B1 : set, (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (baire_step_regular_open_closure X Tx (An n) (Bn n) (xn n) Hreg HxX HBnTx HxBn HAcl HAint).
We prove the intermediate claim HexT: ∃t : set, ∃x1 : set, ∃B1 : set, t = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))).
Apply HexStep to the current goal.
Let x1 be given.
Assume HexB1.
Apply HexB1 to the current goal.
Let B1 be given.
Assume Hpack.
We use (x1,B1) to witness the existential quantifier.
We use x1 to witness the existential quantifier.
We use B1 to witness the existential quantifier.
We prove the intermediate claim HpackP: x1 ∈ (Bn n) ∧ x1 ∉ (An n).
An exact proof term for the current goal is (andEL (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HpackQ: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HpackP.
An exact proof term for the current goal is HpackQ.
We prove the intermediate claim HStep: ∃x1 : set, ∃B1 : set, StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (HStepState_ax n (State n) HexT).
Apply HStep to the current goal.
Let x1 be given.
Assume HexB1.
Apply HexB1 to the current goal.
Let B1 be given.
Assume Hpack.
We prove the intermediate claim Hleft: StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HStateEq: State (ordsucc n) = (x1,B1).
rewrite the current goal using (HState_succ n HnNat) (from left to right).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,B1)) (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) Hleft).
We prove the intermediate claim HB1pack: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HB1pair: B1 ∈ Tx ∧ x1 ∈ B1.
An exact proof term for the current goal is (andEL (B1 ∈ Tx ∧ x1 ∈ B1) (closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) HB1pack).
We prove the intermediate claim HB1Tx: B1 ∈ Tx.
An exact proof term for the current goal is (andEL (B1 ∈ Tx) (x1 ∈ B1) HB1pair).
We prove the intermediate claim Hx1B1: x1 ∈ B1.
An exact proof term for the current goal is (andER (B1 ∈ Tx) (x1 ∈ B1) HB1pair).
We prove the intermediate claim HB1subX: B1 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx B1 HTx HB1Tx).
We prove the intermediate claim Hx1X: x1 ∈ X.
An exact proof term for the current goal is (HB1subX x1 Hx1B1).
We will prove xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx ∧ xn (ordsucc n) ∈ Bn (ordsucc n).
We prove the intermediate claim HxnSucc: xn (ordsucc n) = x1.
We prove the intermediate claim Hdef: xn (ordsucc n) = xcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HStateEq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq x1 B1).
We prove the intermediate claim HBnSucc: Bn (ordsucc n) = B1.
We prove the intermediate claim Hdef: Bn (ordsucc n) = Bcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HStateEq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq x1 B1).
Apply andI to the current goal.
Apply andI to the current goal.
rewrite the current goal using HxnSucc (from left to right).
An exact proof term for the current goal is Hx1X.
rewrite the current goal using HBnSucc (from left to right).
An exact proof term for the current goal is HB1Tx.
rewrite the current goal using HxnSucc (from left to right).
rewrite the current goal using HBnSucc (from left to right).
An exact proof term for the current goal is Hx1B1.
We prove the intermediate claim HInvAllNat: ∀n : set, nat_p n → Inv n.
Set P to be the term (λn0 : set ⇒ Inv n0).
An exact proof term for the current goal is (nat_ind P HInv0 HInvStep).
We prove the intermediate claim HInvAllOmega: ∀n : set, n ∈ ω → Inv n.
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
An exact proof term for the current goal is (HInvAllNat n HnNat).
We prove the intermediate claim Hclosure_succ: ∀n : set, nat_p n → Inv n → closure_of X Tx (Bn (ordsucc n)) ⊆ ((Bn n) ∩ (X ∖ (An n))).
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
We prove the intermediate claim HInvnEq: Inv n = (xn n ∈ X ∧ Bn n ∈ Tx ∧ xn n ∈ Bn n).
Use reflexivity.
We prove the intermediate claim HInvn': xn n ∈ X ∧ Bn n ∈ Tx ∧ xn n ∈ Bn n.
rewrite the current goal using HInvnEq (from right to left).
An exact proof term for the current goal is HInvn.
Apply HInvn' to the current goal.
Assume Hpair HxBn.
Apply Hpair to the current goal.
Assume HxX HBnTx.
We prove the intermediate claim HAnPack: closed_in X Tx (An n) ∧ interior_of X Tx (An n) = Empty.
An exact proof term for the current goal is (HAn n HnO).
We prove the intermediate claim HAcl: closed_in X Tx (An n).
An exact proof term for the current goal is (andEL (closed_in X Tx (An n)) (interior_of X Tx (An n) = Empty) HAnPack).
We prove the intermediate claim HAint: interior_of X Tx (An n) = Empty.
An exact proof term for the current goal is (andER (closed_in X Tx (An n)) (interior_of X Tx (An n) = Empty) HAnPack).
We prove the intermediate claim HexStep: ∃x1 : set, ∃B1 : set, (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (baire_step_regular_open_closure X Tx (An n) (Bn n) (xn n) Hreg HxX HBnTx HxBn HAcl HAint).
We prove the intermediate claim HexT: ∃t : set, ∃x1 : set, ∃B1 : set, t = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))).
Apply HexStep to the current goal.
Let x1 be given.
Assume HexB1.
Apply HexB1 to the current goal.
Let B1 be given.
Assume Hpack.
We use (x1,B1) to witness the existential quantifier.
We use x1 to witness the existential quantifier.
We use B1 to witness the existential quantifier.
We prove the intermediate claim HpackP: x1 ∈ (Bn n) ∧ x1 ∉ (An n).
An exact proof term for the current goal is (andEL (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HpackQ: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HpackP.
An exact proof term for the current goal is HpackQ.
We prove the intermediate claim HStep: ∃x1 : set, ∃B1 : set, StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (HStepState_ax n (State n) HexT).
Apply HStep to the current goal.
Let x1 be given.
Assume HexB1.
Apply HexB1 to the current goal.
Let B1 be given.
Assume Hpack.
We prove the intermediate claim Hleft: StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HStateEq: State (ordsucc n) = (x1,B1).
rewrite the current goal using (HState_succ n HnNat) (from left to right).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,B1)) (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) Hleft).
We prove the intermediate claim HB1pack: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (StepState n (State n) = (x1,B1) ∧ (x1 ∈ (Bn n) ∧ x1 ∉ (An n))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim Hcl: closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (B1 ∈ Tx ∧ x1 ∈ B1) (closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) HB1pack).
We prove the intermediate claim HBnSucc: Bn (ordsucc n) = B1.
We prove the intermediate claim Hdef: Bn (ordsucc n) = Bcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HStateEq (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq x1 B1).
rewrite the current goal using HBnSucc (from left to right).
An exact proof term for the current goal is Hcl.
We prove the intermediate claim Hnesting_succ: ∀n : set, nat_p n → Inv n → Bn (ordsucc n) ⊆ Bn n.
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
We prove the intermediate claim Hcl: closure_of X Tx (Bn (ordsucc n)) ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (Hclosure_succ n HnNat HInvn).
We prove the intermediate claim Hsub: closure_of X Tx (Bn (ordsucc n)) ⊆ (Bn n).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (Bn (ordsucc n))) ((Bn n) ∩ (X ∖ (An n))) (Bn n) Hcl (binintersect_Subq_1 (Bn n) (X ∖ (An n)))).
We prove the intermediate claim HBnsubX: Bn (ordsucc n) ⊆ X.
We prove the intermediate claim HsuccO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n (nat_p_omega n HnNat)).
We prove the intermediate claim HInvSucc: Inv (ordsucc n).
An exact proof term for the current goal is (HInvAllOmega (ordsucc n) HsuccO).
We prove the intermediate claim Hpair: xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx.
An exact proof term for the current goal is (andEL (xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx) (xn (ordsucc n) ∈ Bn (ordsucc n)) HInvSucc).
We prove the intermediate claim HBnTx: Bn (ordsucc n) ∈ Tx.
An exact proof term for the current goal is (andER (xn (ordsucc n) ∈ X) (Bn (ordsucc n) ∈ Tx) Hpair).
An exact proof term for the current goal is (topology_elem_subset X Tx (Bn (ordsucc n)) HTx HBnTx).
An exact proof term for the current goal is (subset_of_set_from_closure_sub X Tx (Bn (ordsucc n)) (Bn n) HTx HBnsubX Hsub).
We prove the intermediate claim Hsub_add_from_base: ∀N0 : set, N0 ∈ ω → ∀k : set, nat_p k → Bn (add_nat k N0) ⊆ Bn N0.
Let N0 be given.
Assume HN0omega: N0 ∈ ω.
We prove the intermediate claim HN0Nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
Let k be given.
Assume HkNat: nat_p k.
Set Pk to be the term (λt : set ⇒ Bn (add_nat t N0) ⊆ Bn N0).
We prove the intermediate claim Hbase: Pk 0.
We prove the intermediate claim HbaseDef: Pk 0 = (Bn (add_nat 0 N0) ⊆ Bn N0).
Use reflexivity.
rewrite the current goal using HbaseDef (from left to right).
We prove the intermediate claim Hadd0: add_nat 0 N0 = N0.
An exact proof term for the current goal is (add_nat_0L N0 HN0Nat).
rewrite the current goal using Hadd0 (from left to right).
An exact proof term for the current goal is (Subq_ref (Bn N0)).
We prove the intermediate claim Hstep: ∀t : set, nat_p t → Pk t → Pk (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume IH: Pk t.
We prove the intermediate claim IHdef: Pk t = (Bn (add_nat t N0) ⊆ Bn N0).
Use reflexivity.
We prove the intermediate claim IH': Bn (add_nat t N0) ⊆ Bn N0.
rewrite the current goal using IHdef (from right to left).
An exact proof term for the current goal is IH.
We prove the intermediate claim HstepDef: Pk (ordsucc t) = (Bn (add_nat (ordsucc t) N0) ⊆ Bn N0).
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate claim HaddS: add_nat (ordsucc t) N0 = ordsucc (add_nat t N0).
An exact proof term for the current goal is (add_nat_SL t HtNat N0 HN0Nat).
rewrite the current goal using HaddS (from left to right).
We prove the intermediate claim HInvn: Inv (add_nat t N0).
An exact proof term for the current goal is (HInvAllNat (add_nat t N0) (add_nat_p t HtNat N0 HN0Nat)).
An exact proof term for the current goal is (Subq_tra (Bn (ordsucc (add_nat t N0))) (Bn (add_nat t N0)) (Bn N0) (Hnesting_succ (add_nat t N0) (add_nat_p t HtNat N0 HN0Nat) HInvn) IH').
An exact proof term for the current goal is (nat_ind Pk Hbase Hstep k HkNat).
We prove the intermediate claim HtailBn: ∀N0 : set, N0 ∈ ω → ∀n : set, n ∈ ω → N0 ⊆ n → xn n ∈ Bn N0.
Let N0 be given.
Assume HN0omega: N0 ∈ ω.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN0subn: N0 ⊆ n.
We prove the intermediate claim HN0Nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim Hexk: ∃k : set, nat_p k ∧ n = add_nat k N0.
An exact proof term for the current goal is (nat_Subq_add_ex N0 HN0Nat n HnNat HN0subn).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair: nat_p k ∧ n = add_nat k N0.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (andEL (nat_p k) (n = add_nat k N0) Hkpair).
We prove the intermediate claim HnEq: n = add_nat k N0.
An exact proof term for the current goal is (andER (nat_p k) (n = add_nat k N0) Hkpair).
rewrite the current goal using HnEq (from left to right).
We prove the intermediate claim HInvnk: Inv (add_nat k N0).
An exact proof term for the current goal is (HInvAllNat (add_nat k N0) (add_nat_p k HkNat N0 HN0Nat)).
We prove the intermediate claim HInvEq: Inv (add_nat k N0) = (xn (add_nat k N0) ∈ X ∧ Bn (add_nat k N0) ∈ Tx ∧ xn (add_nat k N0) ∈ Bn (add_nat k N0)).
Use reflexivity.
We prove the intermediate claim HInv': xn (add_nat k N0) ∈ X ∧ Bn (add_nat k N0) ∈ Tx ∧ xn (add_nat k N0) ∈ Bn (add_nat k N0).
rewrite the current goal using HInvEq (from right to left).
An exact proof term for the current goal is HInvnk.
Apply HInv' to the current goal.
Assume Hpair HxnkBn.
Apply Hpair to the current goal.
Assume HxnkX HBnkTx.
We prove the intermediate claim Hsub: Bn (add_nat k N0) ⊆ Bn N0.
An exact proof term for the current goal is (Hsub_add_from_base N0 HN0omega k HkNat).
An exact proof term for the current goal is (Hsub (xn (add_nat k N0)) HxnkBn).
Set seq to be the term graph ω (λn0 : set ⇒ xn n0).
We prove the intermediate claim Hseq_on: sequence_on seq X.
We prove the intermediate claim Htot: total_function_on seq ω X.
We prove the intermediate claim HxnX: ∀n0 : set, n0 ∈ ω → xn n0 ∈ X.
Let n0 be given.
Assume Hn0O: n0 ∈ ω.
We prove the intermediate claim HInvn0: Inv n0.
An exact proof term for the current goal is (HInvAllOmega n0 Hn0O).
We prove the intermediate claim Hpair: xn n0 ∈ X ∧ Bn n0 ∈ Tx.
An exact proof term for the current goal is (andEL (xn n0 ∈ X ∧ Bn n0 ∈ Tx) (xn n0 ∈ Bn n0) HInvn0).
An exact proof term for the current goal is (andEL (xn n0 ∈ X) (Bn n0 ∈ Tx) Hpair).
We prove the intermediate claim Hdef: seq = graph ω (λn0 : set ⇒ xn n0).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (total_function_on_graph ω X (λn0 : set ⇒ xn n0) HxnX).
An exact proof term for the current goal is (total_function_on_function_on seq ω X Htot).
Set net0 to be the term sequence_as_net seq.
We prove the intermediate claim Hnetdata: directed_set ω (inclusion_rel ω) ∧ total_function_on net0 ω X ∧ functional_graph net0 ∧ graph_domain_subset net0 ω.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is omega_directed_by_inclusion_rel.
We prove the intermediate claim Hg: ∀n0 : set, n0 ∈ ω → apply_fun seq n0 ∈ X.
Let n0 be given.
Assume Hn0: n0 ∈ ω.
We prove the intermediate claim Hfun: function_on seq ω X.
An exact proof term for the current goal is Hseq_on.
An exact proof term for the current goal is (Hfun n0 Hn0).
We prove the intermediate claim Hdef: net0 = graph ω (λn0 : set ⇒ apply_fun seq n0).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (total_function_on_graph ω X (λn0 : set ⇒ apply_fun seq n0) Hg).
We prove the intermediate claim Hdef: net0 = graph ω (λn0 : set ⇒ apply_fun seq n0).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (functional_graph_graph ω (λn0 : set ⇒ apply_fun seq n0)).
We prove the intermediate claim Hdef: net0 = graph ω (λn0 : set ⇒ apply_fun seq n0).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (graph_domain_subset_graph ω (λn0 : set ⇒ apply_fun seq n0)).
Apply (and4E (directed_set ω (inclusion_rel ω)) (total_function_on net0 ω X) (functional_graph net0) (graph_domain_subset net0 ω) Hnetdata) to the current goal.
Assume Hdir Htotnet Hgraphnet Hdomnet.
We prove the intermediate claim Hexacc: ∃xacc : set, accumulation_point_of_net_on X Tx net0 ω (inclusion_rel ω) xacc.
An exact proof term for the current goal is (compact_space_net_has_accumulation_point_on X Tx net0 ω (inclusion_rel ω) Hcomp Hdir Htotnet Hgraphnet Hdomnet).
Apply Hexacc to the current goal.
Let xacc be given.
Assume Hacc: accumulation_point_of_net_on X Tx net0 ω (inclusion_rel ω) xacc.
We prove the intermediate claim Hseq_apply: ∀n0 : set, n0 ∈ ω → apply_fun net0 n0 = xn n0.
Let n0 be given.
Assume Hn0O: n0 ∈ ω.
We prove the intermediate claim Hdef0: net0 = graph ω (λn1 : set ⇒ apply_fun seq n1).
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (apply_fun_graph ω (λn1 : set ⇒ apply_fun seq n1) n0 Hn0O) (from left to right).
We prove the intermediate claim Hseqn: apply_fun seq n0 = xn n0.
We prove the intermediate claim HseqDef: seq = graph ω (λn1 : set ⇒ xn n1).
Use reflexivity.
rewrite the current goal using HseqDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λn1 : set ⇒ xn n1) n0 Hn0O).
An exact proof term for the current goal is Hseqn.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim HclB1: xacc ∈ closure_of X Tx (Bn 1).
We prove the intermediate claim HtailB1: ∀i : set, i ∈ ω → (1,i) ∈ inclusion_rel ω → apply_fun net0 i ∈ Bn 1.
Let i be given.
Assume HiO: i ∈ ω.
Assume H1le: (1,i) ∈ inclusion_rel ω.
We prove the intermediate claim Hsub: 1 ⊆ i.
We prove the intermediate claim Hrel: (1,i) ∈ setprod ω ω ∧ 1 ⊆ i.
An exact proof term for the current goal is (inclusion_relE ω 1 i H1le).
An exact proof term for the current goal is (andER ((1,i) ∈ setprod ω ω) (1 ⊆ i) Hrel).
We prove the intermediate claim Happ: apply_fun net0 i = xn i.
An exact proof term for the current goal is (Hseq_apply i HiO).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (HtailBn 1 H1omega i HiO Hsub).
We prove the intermediate claim HInv1: Inv 1.
An exact proof term for the current goal is (HInvAllOmega 1 H1omega).
We prove the intermediate claim Hpair1: xn 1 ∈ X ∧ Bn 1 ∈ Tx.
An exact proof term for the current goal is (andEL (xn 1 ∈ X ∧ Bn 1 ∈ Tx) (xn 1 ∈ Bn 1) HInv1).
We prove the intermediate claim HBn1Tx: Bn 1 ∈ Tx.
An exact proof term for the current goal is (andER (xn 1 ∈ X) (Bn 1 ∈ Tx) Hpair1).
We prove the intermediate claim HB1subX: Bn 1 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx (Bn 1) HTx HBn1Tx).
An exact proof term for the current goal is (accumulation_point_on_in_closure_of_eventually_terms X Tx net0 ω (inclusion_rel ω) (Bn 1) xacc 1 Hacc HB1subX H1omega HtailB1).
We prove the intermediate claim HclB1subU0: closure_of X Tx (Bn 1) ⊆ U0.
We prove the intermediate claim HclB1subBn0: closure_of X Tx (Bn 1) ⊆ (Bn 0).
We prove the intermediate claim Hcl: closure_of X Tx (Bn 1) ⊆ ((Bn 0) ∩ (X ∖ (An 0))).
An exact proof term for the current goal is (Hclosure_succ 0 nat_0 HInv0).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (Bn 1)) ((Bn 0) ∩ (X ∖ (An 0))) (Bn 0) Hcl (binintersect_Subq_1 (Bn 0) (X ∖ (An 0)))).
We prove the intermediate claim HBn0subU0: Bn 0 ⊆ U0.
rewrite the current goal using HBase_B (from left to right).
An exact proof term for the current goal is (Subq_ref U0).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (Bn 1)) (Bn 0) U0 HclB1subBn0 HBn0subU0).
We prove the intermediate claim HxaccU0: xacc ∈ U0.
An exact proof term for the current goal is (HclB1subU0 xacc HclB1).
We prove the intermediate claim Havoid: ∀n : set, n ∈ ω → xacc ∉ (An n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HsuccO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HclBn: xacc ∈ closure_of X Tx (Bn (ordsucc n)).
We prove the intermediate claim Htail: ∀i : set, i ∈ ω → (ordsucc n,i) ∈ inclusion_rel ω → apply_fun net0 i ∈ Bn (ordsucc n).
Let i be given.
Assume HiO: i ∈ ω.
Assume Hle: (ordsucc n,i) ∈ inclusion_rel ω.
We prove the intermediate claim Hsub: ordsucc n ⊆ i.
We prove the intermediate claim Hrel: (ordsucc n,i) ∈ setprod ω ω ∧ ordsucc n ⊆ i.
An exact proof term for the current goal is (inclusion_relE ω (ordsucc n) i Hle).
An exact proof term for the current goal is (andER ((ordsucc n,i) ∈ setprod ω ω) (ordsucc n ⊆ i) Hrel).
We prove the intermediate claim Happ: apply_fun net0 i = xn i.
An exact proof term for the current goal is (Hseq_apply i HiO).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (HtailBn (ordsucc n) HsuccO i HiO Hsub).
We prove the intermediate claim HInvSn: Inv (ordsucc n).
An exact proof term for the current goal is (HInvAllOmega (ordsucc n) HsuccO).
We prove the intermediate claim HpairSn: xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx.
An exact proof term for the current goal is (andEL (xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx) (xn (ordsucc n) ∈ Bn (ordsucc n)) HInvSn).
We prove the intermediate claim HBnSnTx: Bn (ordsucc n) ∈ Tx.
An exact proof term for the current goal is (andER (xn (ordsucc n) ∈ X) (Bn (ordsucc n) ∈ Tx) HpairSn).
An exact proof term for the current goal is (accumulation_point_on_in_closure_of_eventually_terms X Tx net0 ω (inclusion_rel ω) (Bn (ordsucc n)) xacc (ordsucc n) Hacc (topology_elem_subset X Tx (Bn (ordsucc n)) HTx HBnSnTx) HsuccO Htail).
We prove the intermediate claim Hclsub: closure_of X Tx (Bn (ordsucc n)) ⊆ (X ∖ (An n)).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (Bn (ordsucc n))) ((Bn n) ∩ (X ∖ (An n))) (X ∖ (An n)) (Hclosure_succ n HnNat (HInvAllOmega n HnO)) (binintersect_Subq_2 (Bn n) (X ∖ (An n)))).
We prove the intermediate claim HxaccComp: xacc ∈ (X ∖ (An n)).
An exact proof term for the current goal is (Hclsub xacc HclBn).
An exact proof term for the current goal is (setminusE2 X (An n) xacc HxaccComp).
We use xacc to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HxaccU0.
An exact proof term for the current goal is Havoid.
∎