InformationSystems
Difficulty: hard — 8 definitions, 9 abbreviations, 4 lemmas, 7 theorems, 0 examples.
definition abbreviation lemma theorem
legend
Important
instNormUnit_computerNetworks
instance instNormUnit_computerNetworks : Norm Unit
Show details
| instNormUnit_computerNetworks = { norm := fun x => 0 }
Complexity: 17 (size of the value term)
Outer dependencies: (none)
Lean core dependencies: Unit
Used by: Cell.eraseSecondBit, Cell.erase_not_injective, Cell.erase_not_surjective, Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensorUnit, Component.Hom.tensor_comm, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.empty, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.monoidalCategory, Component.parallel_comm, Component.parallel_empty, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, Receiver.step, Receiver.step_correct, Unit.discrete, instNormNonnegUnit
Important
instNormNonnegUnit
instance instNormNonnegUnit : NormNonneg Unit
Show details
{ nonneg := fun x => le_refl 0 }
Complexity: 25 (size of the value term)
Outer dependencies: NormNonneg, instNormUnit_computerNetworks
Lean core dependencies: Unit
Used by: (none)
Important
instNormProd_computerNetworks
instance instNormProd_computerNetworks.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Norm α] [Norm β] : Norm (α × β)
Show details
| instNormProd_computerNetworks = { norm := fun p => ‖p.1‖ + ‖p.2‖ }
Complexity: 67 (size of the value term)
Outer dependencies: (none)
Lean core dependencies: Prod
Used by: Cell.eraseSecondBit, Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id_comp, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.Simplex.toInformationSystem, Component.empty, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.interchange, Component.monoidalCategory, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast, Component.recast_parallel_left, Component.recast_parallel_right, Component.sequential, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, Discrete.prod, InformationSystem, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, InformationSystem.Step.bottom, InformationSystem.Step.delta_alt, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InformationSystem.parallel, InformationSystem.parallel_delta, InformationSystem.sequential, InformationSystem.sequential_delta, InformationSystem.toSimplex, Receiver.step, Receiver.step_correct, Sender.step, instNormNonnegProd
Important
instNormNonnegProd
instance instNormNonnegProd {α β : Type} [Norm α] [Norm β] [NormNonneg α] [NormNonneg β] : NormNonneg (α × β)
Show details
fun {α β} [Norm α] [Norm β] [NormNonneg α] [NormNonneg β] => { nonneg := fun p => add_nonneg (NormNonneg.nonneg p.1) (NormNonneg.nonneg p.2) }
Complexity: 129 (size of the value term)
Outer dependencies: NormNonneg, instNormProd_computerNetworks
Mathlib dependencies: Norm, Real, add_nonneg
Lean core dependencies: Prod
Used by: (none)
Important
instNormBool_computerNetworks
instance instNormBool_computerNetworks : Norm Bool
Show details
| instNormBool_computerNetworks = { norm := fun x => 0 }
Complexity: 17 (size of the value term)
Outer dependencies: (none)
Lean core dependencies: Bool
Important
instNormNonnegBool
instance instNormNonnegBool : NormNonneg Bool
Show details
{ nonneg := fun x => le_refl 0 }
Complexity: 25 (size of the value term)
Outer dependencies: NormNonneg, instNormBool_computerNetworks
Lean core dependencies: Bool
Used by: (none)
Important
Unit.discrete
theorem Unit.discrete : Discrete Unit
Show details
fun x => Exists.intro 0 (id (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_natCast 0 0 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))))
Complexity: 211 (size of the value term)
Dependencies: Discrete, instNormUnit_computerNetworks
Mathlib dependencies: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Real
Used by: (none)
Important
Bool.discrete
theorem Bool.discrete : Discrete Bool
Show details
fun x => Exists.intro 0 (id (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_natCast 0 0 (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)))))
Complexity: 211 (size of the value term)
Dependencies: Discrete, instNormBool_computerNetworks
Mathlib dependencies: Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Real
Used by: (none)
Important
Discrete.prod
theorem Discrete.prod {α β : Type} [Norm α] [Norm β] (hα : Discrete α) (hβ : Discrete β) : Discrete (α × β)
Show details
fun {α β} [Norm α] [Norm β] hα hβ p => Exists.intro (hα.size p.1 + hβ.size p.2) (id (Eq.mpr (id (congrArg (Eq (‖p.1‖ + ‖p.2‖)) (Nat.cast_add (hα.size p.1) (hβ.size p.2)))) (Eq.mpr (id (congrArg (fun _a => ‖p.1‖ + ‖p.2‖ = _a + ↑(hβ.size p.2)) (Discrete.size_eq hα p.1))) (Eq.mpr (id (congrArg (fun _a => ‖p.1‖ + ‖p.2‖ = ‖p.1‖ + _a) (Discrete.size_eq hβ p.2))) (Eq.refl (‖p.1‖ + ‖p.2‖))))))
Complexity: 2361 (size of the value term)
Dependencies: Discrete, instNormProd_computerNetworks
Proof dependencies: Discrete.size, Discrete.size_eq
Mathlib dependencies: Nat.cast_add, Norm, Real
Used by: (none)
Note
InformationSystem
information-systems
structure InformationSystem (State Input Output : Type) [Norm State] [Norm Input] [Norm Output] [Nonempty State] [Nonempty Input] [Nonempty Output] : Type
step : State → Input → State × Output
conserves : ∀ (s : State) (i : Input), ‖s‖ + ‖i‖ = ‖self.step s i‖
Show details
Outer dependencies: (none)
Inner dependencies: instNormProd_computerNetworks
Used by: Cell.eraseSecondBit, Channel.system, Component, Component.Simplex.toInformationSystem, Component.parallel_comm, InformationSystem.Chain, InformationSystem.Chain.length, InformationSystem.Chain.ofIsChain, InformationSystem.Environment, InformationSystem.Environment.ownState, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, InformationSystem.Run, InformationSystem.Run.cycle, InformationSystem.Run.final, InformationSystem.Run.initial, InformationSystem.Run.toChain, InformationSystem.Run.trajectory, InformationSystem.Run.trajectory_head, InformationSystem.Spontaneous, InformationSystem.Step, InformationSystem.Step.bottom, InformationSystem.Step.delta, InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.delta, InformationSystem.equivalent, InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.eval, InformationSystem.eval_append, InformationSystem.eval_delta, InformationSystem.eval_trichotomy, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, InformationSystem.gatedFlow, InformationSystem.irreversible, InformationSystem.isolated, InformationSystem.natural, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.parallel, InformationSystem.parallel_delta, InformationSystem.perpetuous, InformationSystem.perpetuous_coherent, InformationSystem.reversible, InformationSystem.roundtrip_neutral, InformationSystem.sequential, InformationSystem.sequential_delta, InformationSystem.spontaneous, InformationSystem.spontaneous_no_self_return, InformationSystem.spontaneous_not_perpetuous, InformationSystem.stepAt, InformationSystem.toSimplex, InformationSystem.zero_run_le, Receiver.step, Sender.step, Topology.membership
Note
InformationSystem.Step
structure InformationSystem.Step {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : Type
current : State
input : Input
next : State
output : Output
holds : sys.step self.current self.input = (self.next, self.output)
Show details
Outer dependencies: InformationSystem
Mathlib dependencies: Norm
Used by: InformationSystem.Chain, InformationSystem.Chain.length, InformationSystem.Chain.ofIsChain, InformationSystem.Run, InformationSystem.Run.final, InformationSystem.Run.initial, InformationSystem.Run.toChain, InformationSystem.Run.trajectory, InformationSystem.Step.bottom, InformationSystem.Step.delta, InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.stepAt, Topology.Step.coverageFunctor, Topology.runArrows'
Note
InformationSystem.stepAt
abbrev InformationSystem.stepAt {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) (i : Input) : sys.Step
Show details
| sys.stepAt s i = { current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := ⋯ }
Complexity: 169 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Step
Mathlib dependencies: Norm
Note
InformationSystem.Step.delta
abbrev InformationSystem.Step.delta {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (st : sys.Step) : ℝ
Show details
| st.delta = ‖st.input‖ - ‖st.output‖
Complexity: 145 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Step
Lean core dependencies: Nonempty
Used by: Channel.loss, Channel.lossless_stationary, InformationSystem.Step.delta_alt, InformationSystem.Step.delta_trichotomy, InformationSystem.Step.gains, InformationSystem.Step.loses, InformationSystem.delta, InformationSystem.eval_delta, InformationSystem.parallel_delta, InformationSystem.sequential_delta
Note
InformationSystem.delta
abbrev InformationSystem.delta {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) (i : Input) : ℝ
Show details
| sys.delta s i = (sys.stepAt s i).delta
Complexity: 101 (size of the value term)
Outer dependencies: InformationSystem
Inner dependencies: InformationSystem.Step.delta, InformationSystem.stepAt
Lean core dependencies: Nonempty
Used by: (none)
Important
InformationSystem.Step.delta_trichotomy
theorem InformationSystem.Step.delta_trichotomy {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (st : sys.Step) : st.delta < 0 ∨ st.delta = 0 ∨ st.delta > 0
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {sys} st => lt_trichotomy st.delta 0
Complexity: 113 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta
Mathlib dependencies: Norm, Real, lt_trichotomy
Used by: (none)
Tip
InformationSystem.Step.delta_alt
theorem InformationSystem.Step.delta_alt {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (st : sys.Step) : st.delta = ‖st.next‖ - ‖st.current‖
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {sys} st => have hc := have h := sys.conserves st.current st.input; Eq.mp (congrArg (fun _a => ‖st.current‖ + ‖st.input‖ = ‖_a‖) st.holds) h; id (Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (‖st.input‖ - ‖st.output‖) (‖st.next‖ - ‖st.current‖) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (sub_eq_zero_of_eq hc) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))))
Complexity: 105109 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta
Proof dependencies: instNormProd_computerNetworks
Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq
Important
InformationSystem.Step.loses
theorem InformationSystem.Step.loses {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (st : sys.Step) : st.delta < 0 ↔ ‖st.next‖ < ‖st.current‖
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {sys} st => have hg := InformationSystem.Step.delta_alt st; { mp := fun h => lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.Common.sub_pf Mathlib.Tactic.Ring.Common.neg_zero (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq hg)) (Mathlib.Tactic.Linarith.sub_neg_of_lt h)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))), mpr := fun h => lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (sub_eq_zero_of_eq hg) (Mathlib.Tactic.Linarith.sub_neg_of_lt h)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))) }
Complexity: 103144 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta
Proof dependencies: InformationSystem.Step.delta_alt
Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.add_lt_of_neg_of_le, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Linarith.sub_nonpos_of_le, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, lt_of_not_ge, neg_eq_zero, sub_eq_zero_of_eq
Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Iff, Int, Int.negOfNat, Nat, Nonempty, congrArg, id, inferInstance, rfl
Used by: (none)
Important
InformationSystem.Step.gains
theorem InformationSystem.Step.gains {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (st : sys.Step) : st.delta > 0 ↔ ‖st.next‖ > ‖st.current‖
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {sys} st => have hg := InformationSystem.Step.delta_alt st; { mp := fun h => lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (sub_eq_zero_of_eq hg) (Mathlib.Tactic.Linarith.sub_neg_of_lt h)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))), mpr := fun h => lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.current‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.Common.sub_pf Mathlib.Tactic.Ring.Common.neg_zero (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq hg)) (Mathlib.Tactic.Linarith.sub_neg_of_lt h)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))) }
Complexity: 103142 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Step, InformationSystem.Step.delta
Proof dependencies: InformationSystem.Step.delta_alt
Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.add_lt_of_neg_of_le, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Linarith.sub_nonpos_of_le, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, lt_of_not_ge, neg_eq_zero, sub_eq_zero_of_eq
Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, GT.gt, Iff, Int, Int.negOfNat, Nat, Nonempty, congrArg, id, inferInstance, rfl
Used by: (none)
Important
InformationSystem.Step.bottom
theorem InformationSystem.Step.bottom {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} [NormNonneg State] (st : sys.Step) : ‖st.current‖ = 0 → ‖st.output‖ ≤ ‖st.input‖
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {sys} [NormNonneg State] st hs => have hc := have h := sys.conserves st.current st.input; Eq.mp (congrArg (fun _a => ‖st.current‖ + ‖st.input‖ = ‖_a‖) st.holds) h; have hnn := NormNonneg.nonneg st.next; le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.Common.sub_pf Mathlib.Tactic.Ring.Common.neg_zero (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.current‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.current‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.current‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.current‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.next‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.next‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.next‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.next‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.next‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖st.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖st.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖st.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖st.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖st.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖st.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖st.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.le_of_eq_of_le (Mathlib.Tactic.Linarith.eq_of_eq_of_eq (sub_eq_zero_of_eq hs) (neg_eq_zero.mpr (sub_eq_zero_of_eq hc))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hnn)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))
Complexity: 53382 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Step, NormNonneg
Proof dependencies: instNormProd_computerNetworks
Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.add_lt_of_le_of_neg, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.le_of_eq_of_le, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Linarith.sub_nonpos_of_le, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, le_of_not_gt, neg_eq_zero, sub_eq_zero_of_eq
Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Int, Int.negOfNat, Nat, Nonempty, Prod, congrArg, id, inferInstance, rfl
Used by: (none)
Note
InformationSystem.eval
def InformationSystem.eval {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : State → List Input → State × List Output
Show details
| sys.eval x✝ [] = (x✝, []) | sys.eval x✝ (i :: is) = match sys.step x✝ i with | (s', o) => match sys.eval s' is with | (s'', os) => (s'', o :: os)
Complexity: 99 (size of the value term)
Outer dependencies: InformationSystem
Mathlib dependencies: Norm
Used by: Channel.lossy_loses_overall, Channel.overall_loss, Component.Arrow.setoid, Component.Hom.tensor_id_id, Component.empty_parallel, Component.equivalent_of_stationary, Component.id_sequential, Component.interchange, Component.monoidalCategory, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast_congr, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry_symmetry, InformationSystem.equivalent, InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.eval_append, InformationSystem.eval_delta, InformationSystem.eval_trichotomy, InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.perpetuous, InformationSystem.perpetuous_coherent, InformationSystem.roundtrip_neutral, InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le
Important
InformationSystem.eval_append
theorem InformationSystem.eval_append {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) (is1 is2 : List Input) : (sys.eval s (is1 ++ is2)).1 = (sys.eval (sys.eval s is1).1 is2).1
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] sys s is1 is2 => List.rec (motive := fun is1 => ∀ (s : State), (sys.eval s (is1 ++ is2)).1 = (sys.eval (sys.eval s is1).1 is2).1) (fun s => Eq.refl (sys.eval s ([] ++ is2)).1) (fun i is1 ih s => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg Prod.fst (Eq.trans (InformationSystem.eval.eq_2 sys s i (is1 ++ is2)) (congrFun' (congrArg Prod.mk ((fun s => ih s) (sys.1 s i).1)) ((sys.1 s i).2 :: (sys.eval (sys.1 s i).1 (is1 ++ is2)).2))))) (sys.eval (sys.eval (sys.1 s i).1 is1).1 is2).1) (eq_self (sys.eval (sys.eval (sys.1 s i).1 is1).1 is2).1))) is1 s
Complexity: 2492 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval
Mathlib dependencies: Norm
Note
List.totalSize
abbrev List.totalSize.{u_1} {α : Type u_1} [Norm α] (l : List α) : ℝ
Show details
| l.totalSize = (List.map (fun x => ‖x‖) l).sum
Complexity: 35 (size of the value term)
Outer dependencies: (none)
Important
InformationSystem.eval_trichotomy
theorem InformationSystem.eval_trichotomy {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) (is : List Input) : (sys.eval s is).2.totalSize < is.totalSize ∨ is.totalSize < (sys.eval s is).2.totalSize ∨ is.totalSize = (sys.eval s is).2.totalSize
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] sys s is => Or.casesOn (lt_trichotomy (sys.eval s is).2.totalSize is.totalSize) (fun h => Or.inl h) fun h => Or.casesOn h (fun h => Or.inr (Or.inr (Eq.symm h))) fun h => Or.inr (Or.inl h)
Complexity: 2125 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval, List.totalSize
Mathlib dependencies: Norm, Real, lt_trichotomy
Used by: (none)
Tip
InformationSystem.eval_delta
theorem InformationSystem.eval_delta {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) (is : List Input) : ‖(sys.eval s is).1‖ - ‖s‖ = is.totalSize - (sys.eval s is).2.totalSize
Show details
fun {State} [⋯] [⋯] {Input} [⋯] [⋯] {Output} [⋯] [⋯] sys s is => List.rec (motive := fun is => ∀ (s : State), ‖(sys.eval s is).1‖ - ‖s‖ = is.totalSize - (sys.eval s is).2.totalSize) (fun s => of_eq_true (Eq.trans (congr (congrArg Eq (sub_self ‖s‖)) (sub_self 0)) (eq_self 0))) (fun i is ih s => have hstep := have hc := sys.conserves s i; id (Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (‖(sys.step s i).1‖ - ‖s‖) (‖i‖ - ‖(sys.step s i).2‖) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖i‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖i‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).2‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖i‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖i‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).2‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖i‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖i‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖i‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (sub_eq_zero_of_eq hc) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖i‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖i‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).2‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖i‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖i‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖i‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).2‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).2‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖i‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(sys.step s i).2‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (neg_eq_zero.mpr (sub_eq_zero_of_eq hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))); have hih := ih (sys.step s i).1; id (Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt (‖(sys.eval (sys.step s i).1 is).1‖ - ‖s‖) (‖i‖ + is.totalSize - (‖(sys.step s i).2‖ + (sys.eval (sys.step s i).1 is).2.totalSize)) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.neg_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.eval (sys.step s i).1 is).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf is.totalSize rfl (Eq.mpr (id (congrArg (fun _a => is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = is.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (sys.eval (sys.step s i).1 is).2.totalSize rfl (Eq.mpr (id (congrArg (fun _a => (sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = (sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (sys.eval (sys.step s i).1 is).2.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul is.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (sys.eval (sys.step s i).1 is).2.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (is.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.eval (sys.step s i).1 is).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul is.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (sys.eval (sys.step s i).1 is).2.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 + ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.eval (sys.step s i).1 is).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖i‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf is.totalSize rfl (Eq.mpr (id (congrArg (fun _a => is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = is.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).2‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf (sys.eval (sys.step s i).1 is).2.totalSize rfl (Eq.mpr (id (congrArg (fun _a => (sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = (sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (sys.eval (sys.step s i).1 is).2.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul is.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul (sys.eval (sys.step s i).1 is).2.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (is.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + ((sys.eval (sys.step s i).1 is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖(sys.eval (sys.step s i).1 is).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero is.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (sys.eval (sys.step s i).1 is).2.totalSize (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.Common.add_pf_zero_add 0)))))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.lt_of_eq_of_lt (Mathlib.Tactic.Linarith.eq_of_eq_of_eq (neg_eq_zero.mpr (sub_eq_zero_of_eq hstep)) (neg_eq_zero.mpr (sub_eq_zero_of_eq hih))) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.add_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖s‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) Mathlib.Tactic.Ring.Common.neg_zero)) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.input‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖{ current := s, input := i, next := (sys.step s i).1, output := (sys.step s i).2, holds := InformationSystem.stepAt._proof_1 sys s i }.output‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.eval (sys.step s i).1 is).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.atom_pf ‖(sys.step s i).1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖(sys.step s i).1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖(sys.step s i).1‖ (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.Common.neg_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖(sys.eval (sys.step s i).1 is).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf is.totalSize rfl (Eq.mpr (id (congrArg (fun _a => is.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = is.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (⋯ * ⋯)))) ⋯ ⋯) ⋯) ⋯) ⋯ ⋯) ⋯)) ⋯)))) ⋯ ⋯
Complexity: 389306 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval, List.totalSize
Proof dependencies: InformationSystem.Step.delta, InformationSystem.stepAt
Mathlib dependencies: Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.eq_of_eq_of_eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Linarith.lt_of_eq_of_lt, Mathlib.Tactic.Linarith.sub_neg_of_lt, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_overlap_pf_zero, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.neg_mul, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_zero, Nat.rawCast, Norm, Real, Ring, neg_eq_zero, sub_eq_zero_of_eq, sub_self
Note
InformationSystem.Run
structure InformationSystem.Run {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : Type
steps : List sys.Step
nonempty : self.steps ≠ []
chained : List.IsChain (fun a b => a.next = b.current) self.steps
Show details
Outer dependencies: InformationSystem
Inner dependencies: InformationSystem.Step
Mathlib dependencies: Norm
Note
InformationSystem.Run.initial
abbrev InformationSystem.Run.initial {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (r : sys.Run) : State
Show details
| r.initial = (r.steps.head ⋯).current
Complexity: 165 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Run
Inner dependencies: InformationSystem.Step
Mathlib dependencies: Norm
Note
InformationSystem.Run.final
abbrev InformationSystem.Run.final {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (r : sys.Run) : State
Show details
| r.final = (r.steps.getLast ⋯).next
Complexity: 165 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Run
Inner dependencies: InformationSystem.Step
Mathlib dependencies: Norm
Lean core dependencies: List.getLast, Nonempty
Note
InformationSystem.Run.trajectory
abbrev InformationSystem.Run.trajectory {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (r : sys.Run) : List State
Show details
| r.trajectory = r.initial :: List.map (fun x => x.next) r.steps
Complexity: 195 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Run
Inner dependencies: InformationSystem.Run.initial, InformationSystem.Step
Mathlib dependencies: Norm
Important
InformationSystem.Run.trajectory_head
theorem InformationSystem.Run.trajectory_head {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (r : sys.Run) : r.trajectory.head? = some r.initial
Show details
fun {State} [Nonempty State] [Norm State] {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {sys} r => rfl
Complexity: 105 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Run, InformationSystem.Run.initial, InformationSystem.Run.trajectory
Mathlib dependencies: Norm
Lean core dependencies: Eq, List.head?, Nonempty, Option, rfl
Used by: (none)
Note
InformationSystem.Chain
inductive InformationSystem.Chain {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : State → State → Type
nil : (s : State) → sys.Chain s s
cons : (st : sys.Step) → {s' : State} → sys.Chain st.next s' → sys.Chain st.current s'
Note
InformationSystem.Chain.length
abbrev InformationSystem.Chain.length {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} {s s' : State} : sys.Chain s s' → ℕ
Show details
| (InformationSystem.Chain.nil x✝).length = 0 | (InformationSystem.Chain.cons st rest).length = rest.length + 1
Complexity: 161 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Chain
Inner dependencies: InformationSystem.Step
Mathlib dependencies: Norm
Note
InformationSystem.Chain.ofIsChain
def InformationSystem.Chain.ofIsChain✝ {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (l : List sys.Step) : List.IsChain (fun a b => a.next = b.current) l → (st : sys.Step) → st ∈ l.head? → (stLast : sys.Step) → stLast ∈ l.getLast? → sys.Chain st.current stLast.next
Show details
| InformationSystem.Chain.ofIsChain✝ [] x_6 x x_2 x_1 x_3 = ⋯.elim | InformationSystem.Chain.ofIsChain✝ [a] x_6 x x_2 x_1 x_3 = ⋯ ▸ ⋯ ▸ InformationSystem.Chain.cons a (InformationSystem.Chain.nil a.next) | InformationSystem.Chain.ofIsChain✝ (a :: b :: rest) hchain x x_2 x_1 x_3 = ⋯ ▸ And.casesOn ⋯ fun hr hrest => InformationSystem.Chain.cons a (⋯ ▸ InformationSystem.Chain.ofIsChain✝ (b :: rest) hrest b ⋯ x_1 ⋯)
Complexity: 957 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Chain, InformationSystem.Step
Mathlib dependencies: Norm
Lean core dependencies: And, Eq, Eq.mp, Eq.symm, Eq.trans, False, False.elim, List, List.getLast?, List.getLast?_cons_cons, List.head?, List.head?_cons, Nonempty, Option, Option.mem_def, congrArg, eq_false', noConfusion_of_Nat
Used by: InformationSystem.Run.toChain
Note
InformationSystem.Run.toChain
def InformationSystem.Run.toChain {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (r : sys.Run) : sys.Chain r.initial r.final
Show details
| r.toChain = InformationSystem.Chain.ofIsChain✝ r.steps ⋯ (r.steps.head ⋯) ⋯ (r.steps.getLast ⋯) ⋯
Complexity: 1290 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Chain, InformationSystem.Run, InformationSystem.Run.final, InformationSystem.Run.initial
Inner dependencies: InformationSystem.Chain.ofIsChain, InformationSystem.Step
Mathlib dependencies: Norm
Lean core dependencies: List.getLast, List.getLast_mem_getLast?, List.head, List.head_mem_head?, Nonempty
Used by: Topology.runGrothendieck
Note
InformationSystem.Run.cycle
abbrev InformationSystem.Run.cycle {State : Type} [Nonempty State] [Norm State] {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (r : sys.Run) : Prop
Show details
| r.cycle = (r.initial = r.final)
Complexity: 123 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Run
Inner dependencies: InformationSystem.Run.final, InformationSystem.Run.initial
Mathlib dependencies: Norm
Used by: (none)
Note
InformationSystem.equivalent
def InformationSystem.equivalent {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {State1 State2 : Type} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] (sys1 : InformationSystem State1 Input Output) (sys2 : InformationSystem State2 Input Output) (s1 : State1) (s2 : State2) : Prop
Show details
| sys1.equivalent sys2 s1 s2 = ∀ (is : List Input), (sys1.eval s1 is).2 = (sys2.eval s2 is).2
Complexity: 161 (size of the value term)
Outer dependencies: InformationSystem
Inner dependencies: InformationSystem.eval
Mathlib dependencies: Norm
Used by: Component.Arrow.Equiv, Component.empty_parallel, Component.equivalent_of_stationary, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id_sequential, Component.interchange, Component.monoidalCategory, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.recast_congr, Component.sequential_assoc, Component.sequential_congr, Component.sequential_id, Component.symmetry_symmetry, InformationSystem.equivalent_output, InformationSystem.equivalent_step, InformationSystem.exists_repeat_equivalent
Tip
InformationSystem.equivalent_output
theorem InformationSystem.equivalent_output {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {State1 State2 : Type} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {sys1 : InformationSystem State1 Input Output} {sys2 : InformationSystem State2 Input Output} {s1 : State1} {s2 : State2} (h : sys1.equivalent sys2 s1 s2) (i : Input) : (sys1.step s1 i).2 = (sys2.step s2 i).2
Show details
fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1 State2} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {sys1} {sys2} {s1} {s2} h i => have h1 := h [i]; List.cons.noConfusion h1 fun head_eq tail_eq => eq_of_heq head_eq
Complexity: 410 (size of the value term)
Dependencies: InformationSystem, InformationSystem.equivalent
Proof dependencies: InformationSystem.eval
Mathlib dependencies: Norm
Tip
InformationSystem.equivalent_step
theorem InformationSystem.equivalent_step {Input : Type} [Nonempty Input] [Norm Input] {Output : Type} [Nonempty Output] [Norm Output] {State1 State2 : Type} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {sys1 : InformationSystem State1 Input Output} {sys2 : InformationSystem State2 Input Output} {s1 : State1} {s2 : State2} (h : sys1.equivalent sys2 s1 s2) (i : Input) : sys1.equivalent sys2 (sys1.step s1 i).1 (sys2.step s2 i).1
Show details
fun {Input} [Nonempty Input] [Norm Input] {Output} [Nonempty Output] [Norm Output] {State1 State2} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {sys1} {sys2} {s1} {s2} h i js => have hcons := h (i :: js); List.cons.noConfusion hcons fun head_eq tail_eq => eq_of_heq tail_eq
Complexity: 704 (size of the value term)
Dependencies: InformationSystem, InformationSystem.equivalent
Proof dependencies: InformationSystem.eval
Mathlib dependencies: Norm
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.
definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency
legend