Let X, d, U0, x0 and An be given.
Assume Hcomp: complete_metric_space X d.
Assume HAn: ∀n : set, n ∈ ω → closed_in X (metric_topology X d) (An n) ∧ interior_of X (metric_topology X d) (An n) = Empty.
Assume HU0: U0 ∈ metric_topology X d.
Assume Hx0X: x0 ∈ X.
Assume Hx0U0: x0 ∈ U0.
Set Tx to be the term metric_topology X d.
We prove the intermediate claim Hm: metric_on X d.
An exact proof term for the current goal is (andEL (metric_on X d) (∀seq : set, sequence_on seq X → cauchy_sequence X d seq → ∃x : set, converges_to X (metric_topology X d) seq x) Hcomp).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We prove the intermediate claim HcompConv: ∀seq : set, sequence_on seq X → cauchy_sequence X d seq → ∃x : set, converges_to X Tx seq x.
An exact proof term for the current goal is (andER (metric_on X d) (∀seq : set, sequence_on seq X → cauchy_sequence X d seq → ∃x : set, converges_to X (metric_topology X d) seq x) Hcomp).
Set BaseState to be the term (x0,(0,U0)).
Set xcur to be the term (λst : set ⇒ st 0).
Set rcur to be the term (λst : set ⇒ ((st 1) 0)).
Set Bcur to be the term (λst : set ⇒ ((st 1) 1)).
Set StepState to be the term (λn st : set ⇒ Eps_i (λt : set ⇒ ∃x1 : set, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (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 rn to be the term (λn : set ⇒ rcur (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 (0,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).
We prove the intermediate claim HBcur0: Bcur BaseState = ((BaseState 1) 1).
Use reflexivity.
rewrite the current goal using HBcur0 (from left to right).
rewrite the current goal using (tuple_2_1_eq x0 (0,U0)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq 0 U0) (from left to right) at position 1.
Use reflexivity.
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 HA0pack: closed_in X Tx (An 0) ∧ interior_of X Tx (An 0) = Empty.
An exact proof term for the current goal is (HAn 0 H0omega).
We prove the intermediate claim HA0cl: closed_in X Tx (An 0).
An exact proof term for the current goal is (andEL (closed_in X Tx (An 0)) (interior_of X Tx (An 0) = Empty) HA0pack).
We prove the intermediate claim HA0int: interior_of X Tx (An 0) = Empty.
An exact proof term for the current goal is (andER (closed_in X Tx (An 0)) (interior_of X Tx (An 0) = Empty) HA0pack).
We prove the intermediate claim HexStep0: ∃t : set, ∃x1 : set, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State 0)) ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State 0)) ∩ (X ∖ (An 0)))).
We prove the intermediate claim HU0eq: Bcur (State 0) = U0.
We prove the intermediate claim HBn0: Bn 0 = Bcur (State 0).
Use reflexivity.
rewrite the current goal using HBn0 (from right to left).
rewrite the current goal using HBase_B (from left to right).
Use reflexivity.
We prove the intermediate claim Hex: ∃x1 : set, ∃r1 : set, ∃B1 : set, (x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ (U0 ∩ (X ∖ (An 0)))).
An exact proof term for the current goal is (baire_step_metric_ball_eps_bounded_closure X d (An 0) U0 x0 0 Hm Hx0X HU0 Hx0U0 HA0cl HA0int H0omega).
Apply Hex to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hpack.
We use (x1,(r1,B1)) to witness the existential quantifier.
We use x1 to witness the existential quantifier.
We use r1 to witness the existential quantifier.
We use B1 to witness the existential quantifier.
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim HpackS: (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ (U0 ∩ (X ∖ (An 0)))).
An exact proof term for the current goal is (andER (((x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0)))) ∧ (B1 = open_ball X d x1 r1)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ (U0 ∩ (X ∖ (An 0)))) Hpack).
We prove the intermediate claim HpackL: ((x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0)))) ∧ (B1 = open_ball X d x1 r1).
An exact proof term for the current goal is (andEL (((x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0)))) ∧ (B1 = open_ball X d x1 r1)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ (U0 ∩ (X ∖ (An 0)))) Hpack).
We prove the intermediate claim HpackR: B1 = open_ball X d x1 r1.
An exact proof term for the current goal is (andER ((x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0)))) (B1 = open_ball X d x1 r1) HpackL).
We prove the intermediate claim HpackPQ: (x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0))).
An exact proof term for the current goal is (andEL ((x1 ∈ U0 ∧ x1 ∉ (An 0)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0)))) (B1 = open_ball X d x1 r1) HpackL).
We prove the intermediate claim HpackP: x1 ∈ U0 ∧ x1 ∉ (An 0).
An exact proof term for the current goal is (andEL (x1 ∈ U0 ∧ x1 ∉ (An 0)) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0))) HpackPQ).
We prove the intermediate claim HpackQ: r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0)).
An exact proof term for the current goal is (andER (x1 ∈ U0 ∧ x1 ∉ (An 0)) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc 0))) HpackPQ).
Apply andI to the current goal.
Apply andI to the current goal.
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.
An exact proof term for the current goal is HpackR.
An exact proof term for the current goal is HpackS.
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 HStepState_ax: ∀n st : set, (∃t : set, ∃x1 : set, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n))))) → ∃x1 : set, ∃r1 : set, ∃B1 : set, StepState n st = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (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, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur st) ∩ (X ∖ (An n)))).
Set P to be the term (λt : set ⇒ ∃x1 : set, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur st) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (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 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, ∃r1 : set, ∃B1 : set, (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (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_metric_ball_eps_bounded_closure X d (An n) (Bn n) (xn n) n Hm HxX HBnTx HxBn HAcl HAint HnO).
We prove the intermediate claim HBnDef: Bn n = Bcur (State n).
Use reflexivity.
We prove the intermediate claim HexState: ∃t : set, ∃x1 : set, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))).
Apply HexStep to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hpack.
We use (x1,(r1,B1)) to witness the existential quantifier.
We use x1 to witness the existential quantifier.
We use r1 to witness the existential quantifier.
We use B1 to witness the existential quantifier.
We prove the intermediate claim HpackS: (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)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) ∧ (B1 = open_ball X d x1 r1)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HpackL: ((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) ∧ (B1 = open_ball X d x1 r1).
An exact proof term for the current goal is (andEL (((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) ∧ (B1 = open_ball X d x1 r1)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HpackR: B1 = open_ball X d x1 r1.
An exact proof term for the current goal is (andER ((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HpackL).
We prove the intermediate claim HpackPQ: (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))).
An exact proof term for the current goal is (andEL ((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HpackL).
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)) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HpackPQ).
We prove the intermediate claim HpackQ: r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)).
An exact proof term for the current goal is (andER (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HpackPQ).
We prove the intermediate claim HpackPcur: x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n).
rewrite the current goal using HBnDef (from right to left).
An exact proof term for the current goal is HpackP.
We prove the intermediate claim HpackScur: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n))).
rewrite the current goal using HBnDef (from right to left).
An exact proof term for the current goal is HpackS.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HpackPcur.
An exact proof term for the current goal is HpackQ.
An exact proof term for the current goal is HpackR.
An exact proof term for the current goal is HpackScur.
We prove the intermediate claim HexOut: ∃x1 : set, ∃r1 : set, ∃B1 : set, StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (HStepState_ax n (State n) HexState).
Apply HexOut to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hout.
We prove the intermediate claim HoutS: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim HoutL: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1).
An exact proof term for the current goal is (andEL (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim HoutLL: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))).
An exact proof term for the current goal is (andEL ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HoutL).
We prove the intermediate claim HoutLLL: StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HoutLL).
We prove the intermediate claim HStepEq: StepState n (State n) = (x1,(r1,B1)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1))) (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) HoutLLL).
We prove the intermediate claim HpairTx: B1 ∈ Tx ∧ x1 ∈ B1.
An exact proof term for the current goal is (andEL (B1 ∈ Tx ∧ x1 ∈ B1) (closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) HoutS).
We prove the intermediate claim HB1Tx: B1 ∈ Tx.
An exact proof term for the current goal is (andEL (B1 ∈ Tx) (x1 ∈ B1) HpairTx).
We prove the intermediate claim Hx1B1: x1 ∈ B1.
An exact proof term for the current goal is (andER (B1 ∈ Tx) (x1 ∈ B1) HpairTx).
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 prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).
An exact proof term for the current goal is (HState_succ n HnNat).
We prove the intermediate claim HxnS: xn (ordsucc n) = x1.
We prove the intermediate claim HxnDef: xn (ordsucc n) = xcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using HxnDef (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HxcurDef: xcur (x1,(r1,B1)) = ((x1,(r1,B1)) 0).
Use reflexivity.
rewrite the current goal using HxcurDef (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq x1 (r1,B1)).
We prove the intermediate claim HBnS: Bn (ordsucc n) = B1.
We prove the intermediate claim HBnDef2: Bn (ordsucc n) = Bcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using HBnDef2 (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HBcurDef: Bcur (x1,(r1,B1)) = (((x1,(r1,B1)) 1) 1).
Use reflexivity.
rewrite the current goal using HBcurDef (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (r1,B1)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq r1 B1) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HInvSdef: Inv (ordsucc n) = (xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx ∧ xn (ordsucc n) ∈ Bn (ordsucc n)).
Use reflexivity.
rewrite the current goal using HInvSdef (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
rewrite the current goal using HxnS (from left to right).
An exact proof term for the current goal is Hx1X.
rewrite the current goal using HBnS (from left to right).
An exact proof term for the current goal is HB1Tx.
rewrite the current goal using HxnS (from left to right).
rewrite the current goal using HBnS (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.
Let n be given.
Assume HnNat: nat_p n.
An exact proof term for the current goal is (nat_ind (λk : set ⇒ Inv k) HInv0 (λk HkNat HInvk ⇒ HInvStep k HkNat HInvk) n HnNat).
We prove the intermediate claim HInvAllOmega: ∀n : set, n ∈ ω → Inv n.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (HInvAllNat n (omega_nat_p n HnO)).
We prove the intermediate claim HexState_from_Inv: ∀n : set, nat_p n → Inv n → ∃t : set, ∃x1 : set, ∃r1 : set, ∃B1 : set, t = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An 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, ∃r1 : set, ∃B1 : set, (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (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_metric_ball_eps_bounded_closure X d (An n) (Bn n) (xn n) n Hm HxX HBnTx HxBn HAcl HAint HnO).
We prove the intermediate claim HBnDef: Bn n = Bcur (State n).
Use reflexivity.
Apply HexStep to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hpack.
We use (x1,(r1,B1)) to witness the existential quantifier.
We use x1 to witness the existential quantifier.
We use r1 to witness the existential quantifier.
We use B1 to witness the existential quantifier.
We prove the intermediate claim HpackS: (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)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) ∧ (B1 = open_ball X d x1 r1)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HpackL: ((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) ∧ (B1 = open_ball X d x1 r1).
An exact proof term for the current goal is (andEL (((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) ∧ (B1 = open_ball X d x1 r1)) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n)))) Hpack).
We prove the intermediate claim HpackR: B1 = open_ball X d x1 r1.
An exact proof term for the current goal is (andER ((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HpackL).
We prove the intermediate claim HpackPQ: (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))).
An exact proof term for the current goal is (andEL ((x1 ∈ (Bn n) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HpackL).
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)) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HpackPQ).
We prove the intermediate claim HpackQ: r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)).
An exact proof term for the current goal is (andER (x1 ∈ (Bn n) ∧ x1 ∉ (An n)) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HpackPQ).
We prove the intermediate claim HpackPcur: x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n).
rewrite the current goal using HBnDef (from right to left).
An exact proof term for the current goal is HpackP.
We prove the intermediate claim HpackScur: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n))).
rewrite the current goal using HBnDef (from right to left).
An exact proof term for the current goal is HpackS.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HpackPcur.
An exact proof term for the current goal is HpackQ.
An exact proof term for the current goal is HpackR.
An exact proof term for the current goal is HpackScur.
We prove the intermediate claim HStepOut_from_Inv: ∀n : set, nat_p n → Inv n → ∃x1 : set, ∃r1 : set, ∃B1 : set, StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))).
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
An exact proof term for the current goal is (HStepState_ax n (State n) (HexState_from_Inv n HnNat HInvn)).
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 Hex: ∃x1 : set, ∃r1 : set, ∃B1 : set, StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (HStepOut_from_Inv n HnNat HInvn).
Apply Hex to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hout.
We prove the intermediate claim HoutS: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim Hcl1: closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (B1 ∈ Tx ∧ x1 ∈ B1) (closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) HoutS).
We prove the intermediate claim HoutL: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1).
An exact proof term for the current goal is (andEL (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim HoutLL: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))).
An exact proof term for the current goal is (andEL ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HoutL).
We prove the intermediate claim HoutLLL: StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HoutLL).
We prove the intermediate claim HStepEq: StepState n (State n) = (x1,(r1,B1)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1))) (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) HoutLLL).
We prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).
An exact proof term for the current goal is (HState_succ n HnNat).
We prove the intermediate claim HBnS: Bn (ordsucc n) = B1.
We prove the intermediate claim HBnDef2: Bn (ordsucc n) = Bcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using HBnDef2 (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HBcurDef: Bcur (x1,(r1,B1)) = (((x1,(r1,B1)) 1) 1).
Use reflexivity.
rewrite the current goal using HBcurDef (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (r1,B1)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq r1 B1) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HBnDef: Bn n = Bcur (State n).
Use reflexivity.
rewrite the current goal using HBnS (from left to right).
We prove the intermediate claim Hcl2: closure_of X Tx B1 ⊆ ((Bn n) ∩ (X ∖ (An n))).
rewrite the current goal using HBnDef (from left to right).
An exact proof term for the current goal is Hcl1.
An exact proof term for the current goal is Hcl2.
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 HInvS: Inv (ordsucc n).
An exact proof term for the current goal is (HInvStep n HnNat HInvn).
We prove the intermediate claim HInvSeq: Inv (ordsucc n) = (xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx ∧ xn (ordsucc n) ∈ Bn (ordsucc n)).
Use reflexivity.
We prove the intermediate claim HInvS': xn (ordsucc n) ∈ X ∧ Bn (ordsucc n) ∈ Tx ∧ xn (ordsucc n) ∈ Bn (ordsucc n).
rewrite the current goal using HInvSeq (from right to left).
An exact proof term for the current goal is HInvS.
Apply HInvS' to the current goal.
Assume Hpair HxB.
Apply Hpair to the current goal.
Assume HxX HBnSuccTx.
We prove the intermediate claim HBnSuccSubX: Bn (ordsucc n) ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx (Bn (ordsucc n)) HTx HBnSuccTx).
We prove the intermediate claim HsubInter: Bn (ordsucc n) ⊆ ((Bn n) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (subset_of_set_from_closure_sub X Tx (Bn (ordsucc n)) ((Bn n) ∩ (X ∖ (An n))) HTx HBnSuccSubX Hcl).
An exact proof term for the current goal is (Subq_tra (Bn (ordsucc n)) ((Bn n) ∩ (X ∖ (An n))) (Bn n) HsubInter (binintersect_Subq_1 (Bn n) (X ∖ (An n)))).
We prove the intermediate claim Hradius_succ: ∀n : set, nat_p n → Inv n → rn (ordsucc n) ∈ R ∧ Rlt 0 (rn (ordsucc n)) ∧ Rlt (rn (ordsucc n)) (eps_ (ordsucc n)).
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
We prove the intermediate claim Hex: ∃x1 : set, ∃r1 : set, ∃B1 : set, StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (HStepOut_from_Inv n HnNat HInvn).
Apply Hex to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hout.
We prove the intermediate claim HoutL1: ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1)).
An exact proof term for the current goal is (andEL (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim HoutL2: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))).
An exact proof term for the current goal is (andEL ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HoutL1).
We prove the intermediate claim HQ: r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)).
An exact proof term for the current goal is (andER (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HoutL2).
We prove the intermediate claim HStepEq: StepState n (State n) = (x1,(r1,B1)).
We prove the intermediate claim HoutLLL: StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) (andEL ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HoutL1)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1))) (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) HoutLLL).
We prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).
An exact proof term for the current goal is (HState_succ n HnNat).
We prove the intermediate claim Hrns: rn (ordsucc n) = r1.
We prove the intermediate claim Hrndef: rn (ordsucc n) = rcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using Hrndef (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HrcurDef: rcur (x1,(r1,B1)) = (((x1,(r1,B1)) 1) 0).
Use reflexivity.
rewrite the current goal using HrcurDef (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (r1,B1)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq r1 B1) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hrns (from left to right).
An exact proof term for the current goal is HQ.
We prove the intermediate claim Hball_succ: ∀n : set, nat_p n → Inv n → Bn (ordsucc n) = open_ball X d (xn (ordsucc n)) (rn (ordsucc n)).
Let n be given.
Assume HnNat: nat_p n.
Assume HInvn: Inv n.
We prove the intermediate claim Hex: ∃x1 : set, ∃r1 : set, ∃B1 : set, StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1) ∧ (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))).
An exact proof term for the current goal is (HStepOut_from_Inv n HnNat HInvn).
Apply Hex to the current goal.
Let x1 be given.
Assume Hr1.
Apply Hr1 to the current goal.
Let r1 be given.
Assume HB1.
Apply HB1 to the current goal.
Let B1 be given.
Assume Hout.
We prove the intermediate claim HoutS: B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n))).
An exact proof term for the current goal is (andER (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim HoutL: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1).
An exact proof term for the current goal is (andEL (((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) ∧ (B1 = open_ball X d x1 r1))) (B1 ∈ Tx ∧ x1 ∈ B1 ∧ closure_of X Tx B1 ⊆ ((Bcur (State n)) ∩ (X ∖ (An n)))) Hout).
We prove the intermediate claim HoutLL: (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))).
An exact proof term for the current goal is (andEL ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HoutL).
We prove the intermediate claim HoutLLL: StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n))) HoutLL).
We prove the intermediate claim HStepEq: StepState n (State n) = (x1,(r1,B1)).
An exact proof term for the current goal is (andEL (StepState n (State n) = (x1,(r1,B1))) (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n)) HoutLLL).
We prove the intermediate claim HB1eq: B1 = open_ball X d x1 r1.
An exact proof term for the current goal is (andER ((StepState n (State n) = (x1,(r1,B1)) ∧ (x1 ∈ (Bcur (State n)) ∧ x1 ∉ (An n))) ∧ (r1 ∈ R ∧ Rlt 0 r1 ∧ Rlt r1 (eps_ (ordsucc n)))) (B1 = open_ball X d x1 r1) HoutL).
We prove the intermediate claim HStS: State (ordsucc n) = StepState n (State n).
An exact proof term for the current goal is (HState_succ n HnNat).
We prove the intermediate claim HxnS: xn (ordsucc n) = x1.
We prove the intermediate claim HxnDef: xn (ordsucc n) = xcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using HxnDef (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HxcurDef: xcur (x1,(r1,B1)) = ((x1,(r1,B1)) 0).
Use reflexivity.
rewrite the current goal using HxcurDef (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq x1 (r1,B1)).
We prove the intermediate claim Hrns: rn (ordsucc n) = r1.
We prove the intermediate claim Hrndef: rn (ordsucc n) = rcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using Hrndef (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HrcurDef: rcur (x1,(r1,B1)) = (((x1,(r1,B1)) 1) 0).
Use reflexivity.
rewrite the current goal using HrcurDef (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (r1,B1)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_0_eq r1 B1) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HBnS: Bn (ordsucc n) = B1.
We prove the intermediate claim HBnDef2: Bn (ordsucc n) = Bcur (State (ordsucc n)).
Use reflexivity.
rewrite the current goal using HBnDef2 (from left to right).
rewrite the current goal using HStS (from left to right).
rewrite the current goal using HStepEq (from left to right).
We prove the intermediate claim HBcurDef: Bcur (x1,(r1,B1)) = (((x1,(r1,B1)) 1) 1).
Use reflexivity.
rewrite the current goal using HBcurDef (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 (r1,B1)) (from left to right) at position 1.
rewrite the current goal using (tuple_2_1_eq r1 B1) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HBnS (from left to right).
rewrite the current goal using HB1eq (from left to right).
rewrite the current goal using HxnS (from right to left).
rewrite the current goal using Hrns (from right to left).
Use reflexivity.
Set seq to be the term graph ω (λn : set ⇒ xn n).
We prove the intermediate claim Hseq_on: sequence_on seq X.
Let n be given.
Assume HnO: n ∈ ω.
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ xn k) n HnO) (from left to right).
We prove the intermediate claim HInvn: Inv n.
An exact proof term for the current goal is (HInvAllOmega n HnO).
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.
An exact proof term for the current goal is HxX.
We prove the intermediate claim Hcauchy: cauchy_sequence X d seq.
We prove the intermediate claim HcauchyDef: cauchy_sequence X d seq = (metric_on X d ∧ sequence_on seq X ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps).
Use reflexivity.
rewrite the current goal using HcauchyDef (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
An exact proof term for the current goal is Hseq_on.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < eps.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid eps HepsR HepsPos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < eps) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < eps.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < eps) HNpair).
Set N0 to be the term ordsucc N.
We use N0 to witness the existential quantifier.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
Apply andI to the current goal.
An exact proof term for the current goal is HN0omega.
Let m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume HN0m: N0 ⊆ m.
Assume HN0n: N0 ⊆ n.
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (omega_nat_p m HmO).
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 HN0Nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
We prove the intermediate claim HepsNR: (eps_ N) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsN_Rlt: Rlt (eps_ N) eps.
An exact proof term for the current goal is (RltI (eps_ N) eps HepsNR HepsR HepsNlt).
We prove the intermediate claim Hexkm: ∃km : set, nat_p km ∧ m = add_nat km N0.
An exact proof term for the current goal is (nat_Subq_add_ex N0 HN0Nat m HmNat HN0m).
We prove the intermediate claim Hexkn: ∃kn : set, nat_p kn ∧ n = add_nat kn N0.
An exact proof term for the current goal is (nat_Subq_add_ex N0 HN0Nat n HnNat HN0n).
We prove the intermediate claim HInvN: Inv N.
An exact proof term for the current goal is (HInvAllOmega N HNomega).
We prove the intermediate claim HInvN0: Inv N0.
An exact proof term for the current goal is (HInvStep N (omega_nat_p N HNomega) HInvN).
We prove the intermediate claim HBallN0: Bn N0 = open_ball X d (xn N0) (rn N0).
An exact proof term for the current goal is (Hball_succ N (omega_nat_p N HNomega) HInvN).
We prove the intermediate claim HrN0: rn N0 ∈ R ∧ Rlt 0 (rn N0) ∧ Rlt (rn N0) (eps_ N0).
An exact proof term for the current goal is (Hradius_succ N (omega_nat_p N HNomega) HInvN).
We prove the intermediate claim HrN0lt: Rlt (rn N0) (eps_ N0).
An exact proof term for the current goal is (andER (rn N0 ∈ R ∧ Rlt 0 (rn N0)) (Rlt (rn N0) (eps_ N0)) HrN0).
We prove the intermediate claim HInvN0Eq: Inv N0 = (xn N0 ∈ X ∧ Bn N0 ∈ Tx ∧ xn N0 ∈ Bn N0).
Use reflexivity.
We prove the intermediate claim HInvN0': xn N0 ∈ X ∧ Bn N0 ∈ Tx ∧ xn N0 ∈ Bn N0.
rewrite the current goal using HInvN0Eq (from right to left).
An exact proof term for the current goal is HInvN0.
Apply HInvN0' to the current goal.
Assume HpairN0 HxN0Bn0.
Apply HpairN0 to the current goal.
Assume HxN0X HBnN0Tx.
We prove the intermediate claim HsubBall: Bn N0 ⊆ open_ball X d (xn N0) (eps_ N0).
rewrite the current goal using HBallN0 (from left to right).
An exact proof term for the current goal is (open_ball_radius_mono X d (xn N0) (rn N0) (eps_ N0) HrN0lt).
We prove the intermediate claim Hsub_add: ∀k : set, nat_p k → Bn (add_nat k N0) ⊆ Bn N0.
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).
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) (HInvAllNat (add_nat t N0) (add_nat_p t HtNat N0 HN0Nat))) IH').
An exact proof term for the current goal is (nat_ind Pk Hbase Hstep k HkNat).
Apply Hexkm to the current goal.
Let km be given.
Assume Hkm.
We prove the intermediate claim HkmNat: nat_p km.
An exact proof term for the current goal is (andEL (nat_p km) (m = add_nat km N0) Hkm).
We prove the intermediate claim HmEq: m = add_nat km N0.
An exact proof term for the current goal is (andER (nat_p km) (m = add_nat km N0) Hkm).
Apply Hexkn to the current goal.
Let kn be given.
Assume Hkn.
We prove the intermediate claim HknNat: nat_p kn.
An exact proof term for the current goal is (andEL (nat_p kn) (n = add_nat kn N0) Hkn).
We prove the intermediate claim HnEq: n = add_nat kn N0.
An exact proof term for the current goal is (andER (nat_p kn) (n = add_nat kn N0) Hkn).
rewrite the current goal using HmEq (from left to right).
rewrite the current goal using HnEq (from left to right).
We prove the intermediate claim HmO2: (add_nat km N0) ∈ ω.
An exact proof term for the current goal is (nat_p_omega (add_nat km N0) (add_nat_p km HkmNat N0 HN0Nat)).
We prove the intermediate claim HnO2: (add_nat kn N0) ∈ ω.
An exact proof term for the current goal is (nat_p_omega (add_nat kn N0) (add_nat_p kn HknNat N0 HN0Nat)).
We prove the intermediate claim HseqDef: seq = graph ω (λk : set ⇒ xn k).
Use reflexivity.
We prove the intermediate claim Hseqm: apply_fun seq (add_nat km N0) = xn (add_nat km N0).
An exact proof term for the current goal is (apply_fun_of_graph_eq seq ω (λk : set ⇒ xn k) (add_nat km N0) HseqDef HmO2).
We prove the intermediate claim Hseqn: apply_fun seq (add_nat kn N0) = xn (add_nat kn N0).
An exact proof term for the current goal is (apply_fun_of_graph_eq seq ω (λk : set ⇒ xn k) (add_nat kn N0) HseqDef HnO2).
We prove the intermediate claim HInvm: Inv (add_nat km N0).
An exact proof term for the current goal is (HInvAllOmega (add_nat km N0) HmO2).
We prove the intermediate claim HInvn: Inv (add_nat kn N0).
An exact proof term for the current goal is (HInvAllOmega (add_nat kn N0) HnO2).
We prove the intermediate claim HInvmEq: Inv (add_nat km N0) = (xn (add_nat km N0) ∈ X ∧ Bn (add_nat km N0) ∈ Tx ∧ xn (add_nat km N0) ∈ Bn (add_nat km N0)).
Use reflexivity.
We prove the intermediate claim HInvnEq: Inv (add_nat kn N0) = (xn (add_nat kn N0) ∈ X ∧ Bn (add_nat kn N0) ∈ Tx ∧ xn (add_nat kn N0) ∈ Bn (add_nat kn N0)).
Use reflexivity.
We prove the intermediate claim HInvm': xn (add_nat km N0) ∈ X ∧ Bn (add_nat km N0) ∈ Tx ∧ xn (add_nat km N0) ∈ Bn (add_nat km N0).
rewrite the current goal using HInvmEq (from right to left).
An exact proof term for the current goal is HInvm.
We prove the intermediate claim HInvn': xn (add_nat kn N0) ∈ X ∧ Bn (add_nat kn N0) ∈ Tx ∧ xn (add_nat kn N0) ∈ Bn (add_nat kn N0).
rewrite the current goal using HInvnEq (from right to left).
An exact proof term for the current goal is HInvn.
Apply HInvm' to the current goal.
Assume Hpairm HxmBm.
Apply Hpairm to the current goal.
Assume HxmX HBmTx.
Apply HInvn' to the current goal.
Assume Hpairn HxnBn.
Apply Hpairn to the current goal.
Assume HxnX HBnTx2.
We prove the intermediate claim Hsubm: Bn (add_nat km N0) ⊆ Bn N0.
An exact proof term for the current goal is (Hsub_add km HkmNat).
We prove the intermediate claim Hsubn: Bn (add_nat kn N0) ⊆ Bn N0.
An exact proof term for the current goal is (Hsub_add kn HknNat).
We prove the intermediate claim HxmBN0: xn (add_nat km N0) ∈ Bn N0.
An exact proof term for the current goal is (Hsubm (xn (add_nat km N0)) HxmBm).
We prove the intermediate claim HxnBN0: xn (add_nat kn N0) ∈ Bn N0.
An exact proof term for the current goal is (Hsubn (xn (add_nat kn N0)) HxnBn).
We prove the intermediate claim HxmBig: xn (add_nat km N0) ∈ open_ball X d (xn N0) (eps_ N0).
An exact proof term for the current goal is (HsubBall (xn (add_nat km N0)) HxmBN0).
We prove the intermediate claim HxnBig: xn (add_nat kn N0) ∈ open_ball X d (xn N0) (eps_ N0).
An exact proof term for the current goal is (HsubBall (xn (add_nat kn N0)) HxnBN0).
We prove the intermediate claim HxN0X': xn N0 ∈ X.
An exact proof term for the current goal is HxN0X.
rewrite the current goal using Hseqm (from left to right).
rewrite the current goal using Hseqn (from left to right).
We prove the intermediate claim Hdist: Rlt (apply_fun d (xn (add_nat km N0),xn (add_nat kn N0))) (eps_ N).
An exact proof term for the current goal is (open_ball_pair_dist_lt_eps_pred X d (xn N0) N (xn (add_nat km N0)) (xn (add_nat kn N0)) Hm HxN0X' HNomega HxmBig HxnBig).
An exact proof term for the current goal is (Rlt_tra (apply_fun d (xn (add_nat km N0),xn (add_nat kn N0))) (eps_ N) eps Hdist HepsN_Rlt).
We prove the intermediate claim Hexlim: ∃x : set, converges_to X Tx seq x.
An exact proof term for the current goal is (HcompConv seq Hseq_on Hcauchy).
Apply Hexlim to the current goal.
Let xlim be given.
Assume Hxlim: converges_to X Tx seq xlim.
We use xlim to witness the existential quantifier.
We prove the intermediate claim HseqDef: seq = graph ω (λn0 : set ⇒ xn n0).
Use reflexivity.
We prove the intermediate claim Hseq_apply: ∀n : set, n ∈ ω → apply_fun seq n = xn n.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (apply_fun_of_graph_eq seq ω (λn0 : set ⇒ xn n0) n HseqDef HnO).
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).
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) (HInvAllNat (add_nat t N0) (add_nat_p t HtNat N0 HN0Nat))) 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).
Apply andI to the current goal.
We will prove xlim ∈ U0.
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 HtailB1: ∀n : set, n ∈ ω → 1 ⊆ n → apply_fun seq n ∈ Bn 1.
Let n be given.
Assume HnO: n ∈ ω.
Assume H1subn: 1 ⊆ n.
We prove the intermediate claim Hseqn: apply_fun seq n = xn n.
An exact proof term for the current goal is (Hseq_apply n HnO).
rewrite the current goal using Hseqn (from left to right).
An exact proof term for the current goal is (HtailBn 1 H1omega n HnO H1subn).
We prove the intermediate claim HxlimClB1: xlim ∈ closure_of X Tx (Bn 1).
An exact proof term for the current goal is (converges_to_imp_in_closure_of_eventually_terms X Tx (Bn 1) seq xlim 1 Hxlim H1omega HtailB1).
We prove the intermediate claim HclB1: 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).
We prove the intermediate claim HclB1subBn0: closure_of X Tx (Bn 1) ⊆ (Bn 0).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (Bn 1)) ((Bn 0) ∩ (X ∖ (An 0))) (Bn 0) HclB1 (binintersect_Subq_1 (Bn 0) (X ∖ (An 0)))).
We prove the intermediate claim HclB1subU0: closure_of X Tx (Bn 1) ⊆ U0.
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).
An exact proof term for the current goal is (HclB1subU0 xlim HxlimClB1).
Let n be given.
Assume HnO: n ∈ ω.
We will prove xlim ∉ (An n).
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 HtailBsucc: ∀m : set, m ∈ ω → ordsucc n ⊆ m → apply_fun seq m ∈ Bn (ordsucc n).
Let m be given.
Assume HmO: m ∈ ω.
Assume Hsub: ordsucc n ⊆ m.
We prove the intermediate claim Hseqm: apply_fun seq m = xn m.
An exact proof term for the current goal is (Hseq_apply m HmO).
rewrite the current goal using Hseqm (from left to right).
An exact proof term for the current goal is (HtailBn (ordsucc n) HsuccO m HmO Hsub).
We prove the intermediate claim HxlimCl: xlim ∈ closure_of X Tx (Bn (ordsucc n)).
An exact proof term for the current goal is (converges_to_imp_in_closure_of_eventually_terms X Tx (Bn (ordsucc n)) seq xlim (ordsucc n) Hxlim HsuccO HtailBsucc).
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 HInvn: Inv n.
An exact proof term for the current goal is (HInvAllOmega n HnO).
We prove the intermediate claim HclEq: 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 HsubComp: 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)) HclEq (binintersect_Subq_2 (Bn n) (X ∖ (An n)))).
We prove the intermediate claim HxlimComp: xlim ∈ (X ∖ (An n)).
An exact proof term for the current goal is (HsubComp xlim HxlimCl).
An exact proof term for the current goal is (setminusE2 X (An n) xlim HxlimComp).
∎