Perpetuity
Difficulty: hard — 7 definitions, 1 abbreviations, 4 lemmas, 7 theorems, 0 examples.
definition abbreviation lemma theorem
legend
Note
InformationSystem.perpetuous
def InformationSystem.perpetuous {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) : Prop
Show details
| sys.perpetuous s = ∀ (is : List Input), ∃ is', (∀ i ∈ is', ‖i‖ = 0) ∧ (sys.eval s (is ++ is')).1 = s
Complexity: 175 (size of the value term)
Outer dependencies: InformationSystem
Inner dependencies: InformationSystem.eval
Tip
InformationSystem.roundtrip_neutral
theorem InformationSystem.roundtrip_neutral {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (s : State) (is : List Input) (hreturn : (sys.eval s is).1 = s) : is.totalSize = (sys.eval s is).2.totalSize
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys s is hreturn => have h := InformationSystem.eval_delta sys s is; Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt is.totalSize (sys.eval s 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.sub_congr (Mathlib.Tactic.Ring.Common.sub_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 ‖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_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_zero_add 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 s is).2.totalSize rfl (Eq.mpr (id (congrArg (fun _a => (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl ((sys.eval s 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 s 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 s 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 s 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_zero_add (is.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + ((sys.eval s is).2.totalSize ^ 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 s is).2.totalSize rfl (Eq.mpr (id (congrArg (fun _a => (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl ((sys.eval s 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 s 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 s is).2.totalSize ^ 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 is.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_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero (sys.eval s is).2.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_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 (Eq.mp (congrArg (fun _a => ‖_a‖ - ‖s‖ = is.totalSize - (sys.eval s is).2.totalSize) hreturn) h)) (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.sub_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 ‖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_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_zero_add 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 s is).2.totalSize rfl (Eq.mpr (id (congrArg (fun _a => (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl ((sys.eval s 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 s 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 s 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 s 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_zero_add (is.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + ((sys.eval s is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (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 s 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.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf (sys.eval s is).2.totalSize rfl (Eq.mpr (id (congrArg (fun _a => (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * Nat.rawCast 1 = (sys.eval s is).2.totalSize ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl ((sys.eval s is).2.totalSize ^ 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.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_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_gt (is.totalSize ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.Common.add_pf_add_zero ((sys.eval s 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 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 s 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 (neg_eq_zero.mpr (sub_eq_zero_of_eq (Eq.mp (congrArg (fun _a => ‖_a‖ - ‖s‖ = is.totalSize - (sys.eval s is).2.totalSize) hreturn) h))) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))
Complexity: 57814 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval, List.totalSize, NormNonneg
Proof dependencies: InformationSystem.eval_delta
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.perpetuous_coherent
theorem InformationSystem.perpetuous_coherent {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (s : State) (hp : sys.perpetuous s) (is : List Input) : ∃ is', (is ++ is').totalSize = (sys.eval s (is ++ is')).2.totalSize
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys s hp is => Exists.casesOn (hp is) fun is' h => And.casesOn h fun left hret => Exists.intro is' (InformationSystem.roundtrip_neutral sys s (is ++ is') hret)
Complexity: 1189 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval, InformationSystem.perpetuous, List.totalSize, NormNonneg
Proof dependencies: InformationSystem.roundtrip_neutral
Used by: (none)
Note
InformationSystem.Spontaneous
inductive InformationSystem.Spontaneous {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : State → Prop
bottom : ∀ {s : State}, ‖s‖ = 0 → sys.Spontaneous s
decay : ∀ {s : State}, (∀ (i : Input), ‖i‖ = 0 → ‖(sys.step s i).1‖ < ‖s‖) → sys.Spontaneous s
next : ∀ {s : State}, (∀ (i : Input), ‖i‖ = 0 → sys.Spontaneous (sys.step s i).1) → sys.Spontaneous s
Show details
Outer dependencies: InformationSystem
Note
InformationSystem.spontaneous
def InformationSystem.spontaneous {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : Prop
Show details
| sys.spontaneous = ∀ (s : State), sys.Spontaneous s
Complexity: 75 (size of the value term)
Outer dependencies: InformationSystem
Inner dependencies: InformationSystem.Spontaneous
Mathlib dependencies: Norm
Lean core dependencies: Nonempty
Tip
InformationSystem.zero_run_le
theorem InformationSystem.zero_run_le {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (s : State) (is : List Input) (hzero : ∀ i ∈ is, ‖i‖ = 0) : ‖(sys.eval s is).1‖ ≤ ‖s‖
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys s is hzero => List.rec (motive := fun is => ∀ (s : State), (∀ i ∈ is, ‖i‖ = 0) → ‖(sys.eval s is).1‖ ≤ ‖s‖) (fun s hzero => of_eq_true (Std.le_refl._simp_1 ‖s‖)) (fun i is ih s hzero => have hi := hzero i List.mem_cons_self; have hstep := have h := sys.conserves s i; have hnn := NormNonneg.nonneg (sys.step s i).2; 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 ‖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.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 (‖i‖ ^ 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 ‖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_gt (‖i‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_add_zero (‖s‖ ^ 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 (‖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 (‖(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 ‖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 ‖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 ‖(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.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_zero_add (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + (‖(sys.step s i).1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + (‖(sys.step s i).2‖ ^ 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 ‖(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_zero_add (‖(sys.step s i).2‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ 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_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.Common.sub_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 ‖(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_lt (‖s‖ ^ 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 + 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 ‖(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_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 hi) (neg_eq_zero.mpr (sub_eq_zero_of_eq h))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hnn)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))); have this := ih (sys.step s i).1 fun j hj => hzero j (List.mem_cons_of_mem i hj); id (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.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 ‖(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.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_lt (‖s‖ ^ 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 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.Common.sub_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 ‖(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.sub_pf (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_zero) (Mathlib.Tactic.Ring.Common.add_pf_add_lt (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.Common.add_pf_zero_add (‖(sys.eval (sys.step s i).1 is).1‖ ^ 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 ‖(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.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.add_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le hstep) (Mathlib.Tactic.Linarith.sub_nonpos_of_le this)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))) is s hzero
Complexity: 82268 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval, NormNonneg
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.add_nonpos, 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_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, 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, List, List.mem_cons_of_mem, List.mem_cons_self, Nat, Nonempty, congrArg, id, inferInstance, of_eq_true, rfl
Tip
InformationSystem.spontaneous_no_self_return
theorem InformationSystem.spontaneous_no_self_return {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (s : State) (hspon : sys.Spontaneous s) : 0 < ‖s‖ → ∀ (is : List Input), is ≠ [] → (∀ i ∈ is, ‖i‖ = 0) → (sys.eval s is).1 ≠ s
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys s hspon => InformationSystem.Spontaneous.rec (motive := fun s hspon => 0 < ‖s‖ → ∀ (is : List Input), is ≠ [] → (∀ i ∈ is, ‖i‖ = 0) → (sys.eval s is).1 ≠ s) (fun {s} h hpos => False.elim (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.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.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 (‖s‖ ^ 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 ‖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_zero_add (‖s‖ ^ 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.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 (sub_eq_zero_of_eq h) (Mathlib.Tactic.Linarith.sub_neg_of_lt hpos))))) (fun {s} hlt a is hne hzero => match is, hne, hzero with | i :: is, x, hzero => have hi := hzero i List.mem_cons_self; have hd := hlt i hi; have hle := InformationSystem.zero_run_le sys (sys.step s i).1 is fun j hj => hzero j (List.mem_cons_of_mem i hj); id fun heq => False.elim (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.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 ‖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 ‖(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 (‖s‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 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 ‖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_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.sub_neg_of_lt hd) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Eq.mp (congrArg (fun _a => ‖_a‖ ≤ ‖(sys.step s i).1‖) heq) hle)))))) (fun {s} hnext ih hpos is hne hzero => match is, hne, hzero with | i :: is, x, hzero => have hi := hzero i List.mem_cons_self; have hzero' := fun j hj => hzero j (List.mem_cons_of_mem i hj); id fun heq => let s1 := (sys.step s i).1; have hs1 := rfl; have hs1_le_s := InformationSystem.zero_run_le sys s [i] (Eq.mpr (id (Eq.trans (forall_congr fun i_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (i_1 = i)) List.not_mem_nil._simp_1) (or_false (i_1 = i)))) (Eq.refl (‖i_1‖ = 0))) forall_eq._simp_1)) hi); have hs_le_s1 := have hle := InformationSystem.zero_run_le sys s1 is hzero'; 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.sub_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 ‖s1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s1‖ (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_zero_add (‖s1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖s1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s1‖ ^ 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 (‖s1‖ ^ 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 ‖s1‖ (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_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Eq.mp (congrArg (fun _a => ‖_a‖ ≤ ‖s1‖) (Eq.mp (congrArg (fun _a => (sys.eval _a is).1 = s) (have this := rfl; this)) heq)) hle)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))); have hpos1 := 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.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (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_zero_add (‖s‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.Common.sub_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 ‖s1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1)))) (Mathlib.Tactic.Ring.Common.sub_pf (Mathlib.Tactic.Ring.Common.neg_add (Mathlib.Tactic.Ring.Common.neg_mul ‖s1‖ (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_zero_add (‖s1‖ ^ 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_zero_add (‖s1‖ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.Common.sub_congr (Mathlib.Tactic.Ring.Common.atom_pf ‖s1‖ rfl (Eq.mpr (id (congrArg (fun _a => ‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 = ‖s1‖ ^ Nat.rawCast 1 * _a) (Eq.symm rfl))) (Eq.refl (‖s1‖ ^ 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 (‖s1‖ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.Common.add_overlap_pf_zero ‖s1‖ (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.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.sub_neg_of_lt hpos) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hs_le_s1)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))); have heq' := Eq.mp (congrArg (fun _a => (sys.eval _a is).1 = s) (have this := rfl; this)) heq; have hrot := Eq.mpr (id (congrArg (fun _a => _a = s1) (InformationSystem.eval_append sys s1 is [i]))) (Eq.mpr (id (congrArg (fun _a => (sys.eval _a [i]).1 = s1) heq')) (Eq.refl (sys.eval s [i]).1)); have hne' := of_eq_true (Eq.trans (congrArg Not (Eq.trans List.append_eq_nil_iff._simp_1 (Eq.trans (congrArg (And (is = [])) (List.cons_ne_self._simp_1 i [])) (and_false (is = []))))) not_false_eq_true); have hzero'' := fun j hj => Or.casesOn (List.mem_append.mp hj) (fun hj => hzero' j hj) fun hj => Eq.mpr (id (congrArg (fun _a => ‖_a‖ = 0) (List.mem_singleton.mp hj))) hi; ih i hi hpos1 (is ++ [i]) hne' hzero'' hrot) hspon
Complexity: 61988 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Spontaneous, InformationSystem.eval, NormNonneg
Proof dependencies: InformationSystem.eval_append, InformationSystem.zero_run_le
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.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Linarith.add_lt_of_le_of_neg, 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_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, lt_of_not_ge, sub_eq_zero_of_eq
Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, False.elim, Int, Int.negOfNat, List, List.mem_append, List.mem_cons_of_mem, List.mem_cons_self, List.mem_singleton, Nat, Ne, Nonempty, Not, Or, True, absurd, and_false, congrArg, forall_congr, id, implies_congr, inferInstance, not_false_eq_true, of_eq_true, or_false, rfl
Important
InformationSystem.not_spontaneous_and_perpetuous
theorem InformationSystem.not_spontaneous_and_perpetuous {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (s : State) (hpos : 0 < ‖s‖) (i0 : Input) (hi0 : ‖i0‖ = 0) : ¬(sys.Spontaneous s ∧ sys.perpetuous s)
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys s hpos i0 hi0 a => And.casesOn a fun hspon hperp => Exists.casesOn (hperp [i0]) fun is' h => And.casesOn h fun hzero hret => have hzero' := fun i hi => Or.casesOn (List.eq_or_mem_of_mem_cons hi) (fun h => Eq.ndrec (motive := fun i0 => ‖i0‖ = 0 → (sys.eval s (i0 :: is')).1 = s → i ∈ i0 :: is' → ‖i‖ = 0) (fun hi0 hret hi => hi0) h hi0 hret hi) fun hi => hzero i hi; InformationSystem.spontaneous_no_self_return sys s hspon hpos (i0 :: is') (of_eq_true (Eq.trans (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat List.ctorIdx h))) not_false_eq_true)) hzero' hret
Complexity: 1682 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Spontaneous, InformationSystem.perpetuous, NormNonneg
Proof dependencies: InformationSystem.eval, InformationSystem.spontaneous_no_self_return
Lean core dependencies: And, Eq, Eq.trans, Exists, False, False.elim, List, List.eq_or_mem_of_mem_cons, Nonempty, Not, Or, True, congrArg, eq_false', noConfusion_of_Nat, not_false_eq_true, of_eq_true
Important
InformationSystem.spontaneous_not_perpetuous
theorem InformationSystem.spontaneous_not_perpetuous {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (hspon : sys.spontaneous) (s : State) (hpos : 0 < ‖s‖) (i0 : Input) (hi0 : ‖i0‖ = 0) : ¬sys.perpetuous s
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys hspon s hpos i0 hi0 hperp => InformationSystem.not_spontaneous_and_perpetuous sys s hpos i0 hi0 ⟨hspon s, hperp⟩
Complexity: 259 (size of the value term)
Dependencies: InformationSystem, InformationSystem.perpetuous, InformationSystem.spontaneous, NormNonneg
Proof dependencies: InformationSystem.Spontaneous, InformationSystem.not_spontaneous_and_perpetuous
Used by: (none)
Note
InformationSystem.Environment
structure InformationSystem.Environment {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : Type 1
EnvState : Type
nonempty : Nonempty self.EnvState
size : Norm self.EnvState
system : InformationSystem self.EnvState Output Input
Note
InformationSystem.Environment.universe
def InformationSystem.Environment.universe {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (env : sys.Environment) : InformationSystem (((State × env.EnvState) × Input) × Output) Unit Unit
Show details
| env.universe = { step := fun x x_1 => match x with | (((s, e), i), o) => match sys.step s i with | (s', o') => match env.system.step e o with | (e', i') => ((((s', e'), i'), o'), ()), conserves := ⋯ }
Complexity: 933 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Environment, instNormProd_computerNetworks, instNormUnit_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_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
Note
InformationSystem.isolated
def InformationSystem.isolated {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) : Prop
Show details
| sys.isolated = ∀ (s : State) (i : Input), ‖i‖ = 0 ∧ ‖(sys.step s i).2‖ = 0
Complexity: 133 (size of the value term)
Outer dependencies: InformationSystem
Important
InformationSystem.Environment.universe_isolated
theorem InformationSystem.Environment.universe_isolated {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] {sys : InformationSystem State Input Output} (env : sys.Environment) : env.universe.isolated
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] {sys} env x x_1 => ⟨rfl, rfl⟩
Complexity: 953 (size of the value term)
Dependencies: InformationSystem, InformationSystem.Environment, InformationSystem.Environment.universe, InformationSystem.isolated, NormNonneg, instNormProd_computerNetworks, instNormUnit_computerNetworks
Used by: (none)
Note
InformationSystem.Environment.ownState
abbrev InformationSystem.Environment.ownState {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] {sys : InformationSystem State Input Output} (env : sys.Environment) (w : ((State × env.EnvState) × Input) × Output) : State
Show details
| env.ownState w = w.1.1.1
Complexity: 205 (size of the value term)
Outer dependencies: InformationSystem, InformationSystem.Environment
Mathlib dependencies: Norm
Used by: (none)
Note
InformationSystem.natural
def InformationSystem.natural {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] (sys : InformationSystem State Input Output) (s : State) : Prop
Show details
| sys.natural s = (sys.Spontaneous s ∧ ∃ env, ∀ (e : env.EnvState) (i : Input), ‖i‖ = 0 → ‖(env.system.step e (sys.step s i).2).1‖ - ‖e‖ = ‖s‖ - ‖(sys.step s i).1‖)
Complexity: 525 (size of the value term)
Outer dependencies: InformationSystem
Inner dependencies: InformationSystem.Environment, InformationSystem.Spontaneous
Used by: (none)
Important
InformationSystem.irreversible
theorem InformationSystem.irreversible {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (s1 s2 : State) (i1 i2 : Input) (hne : (s1, i1) ≠ (s2, i2)) (hcol : sys.step s1 i1 = sys.step s2 i2) (recover : State × Output → State × Input) (hrecover : ∀ (s : State) (i : Input), recover (sys.step s i) = (s, i)) : False
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys s1 s2 i1 i2 hne hcol recover hrecover => hne (Eq.mpr (id (congrArg (fun _a => _a = (s2, i2)) (Eq.symm (hrecover s1 i1)))) (Eq.mpr (id (congrArg (fun _a => recover _a = (s2, i2)) hcol)) (Eq.mpr (id (congrArg (fun _a => _a = (s2, i2)) (hrecover s2 i2))) (Eq.refl (s2, i2)))))
Complexity: 1047 (size of the value term)
Dependencies: InformationSystem, NormNonneg
Mathlib dependencies: Norm
Used by: (none)
Important
InformationSystem.reversible
theorem InformationSystem.reversible {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] (sys : InformationSystem State Input Output) (hinj : Function.Injective fun p => sys.step p.1 p.2) : ∃ recover, ∀ (s : State) (i : Input), recover (sys.step s i) = (s, i)
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] sys hinj => Exists.intro (Function.invFun fun p => sys.step p.1 p.2) fun s i => Function.leftInverse_invFun hinj (s, i)
Complexity: 353 (size of the value term)
Dependencies: InformationSystem, NormNonneg
Mathlib dependencies: Function.invFun, Function.leftInverse_invFun, Norm
Lean core dependencies: Eq, Exists, Function.Injective, Nonempty, Prod
Used by: (none)
Tip
InformationSystem.exists_repeat_state
theorem InformationSystem.exists_repeat_state {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] [Fintype State] (sys : InformationSystem State Input Output) (s : State) (is : List Input) (hlen : Fintype.card State < is.length) : ∃ i j, i < j ∧ j ≤ is.length ∧ (sys.eval s (List.take i is)).1 = (sys.eval s (List.take j is)).1
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] [Fintype State] sys s is hlen => have hcard := of_eq_true (Eq.trans (Eq.trans (congrArg (LT.lt (Fintype.card State)) (Fintype.card_fin (Fintype.card State + 1))) (lt_add_iff_pos_right._simp_1 (Fintype.card State))) (Eq.trans Order.lt_one_iff._simp_1 (eq_self 0))); Exists.casesOn (Fintype.exists_ne_map_eq_of_card_lt (fun k => (sys.eval s (List.take (↑k) is)).1) hcard) fun x h => Exists.casesOn h fun y h => And.casesOn h fun hxy hfxy => have hx := x.isLt; have hy := y.isLt; Or.casesOn (lt_or_gt_of_ne fun h => hxy (Fin.ext h)) (fun hlt => Exists.intro (↑x) (Exists.intro ↑y ⟨hlt, ⟨Decidable.byContradiction fun a => InformationSystem.exists_repeat_state._proof_1_1 is hlen x y hy a, hfxy⟩⟩)) fun hgt => Exists.intro (↑y) (Exists.intro ↑x ⟨hgt, ⟨Decidable.byContradiction fun a => InformationSystem.exists_repeat_state._proof_1_2 is hlen x y hx a, Eq.symm hfxy⟩⟩)
Complexity: 6996 (size of the value term)
Dependencies: InformationSystem, InformationSystem.eval, NormNonneg
Mathlib dependencies: Fintype, Fintype.card, Fintype.card_fin, Fintype.exists_ne_map_eq_of_card_lt, Norm, lt_or_gt_of_ne
Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.symm, Eq.trans, Exists, Fin, Fin.ext, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, List, List.length, List.take, Nat, Nat.cast, Nat.lt_of_not_le, Ne, Nonempty, Not, Or, True, congrArg, eq_self, id, le_of_le_of_eq, of_decide_eq_true, of_eq_true
Important
InformationSystem.exists_repeat_equivalent
theorem InformationSystem.exists_repeat_equivalent {State Input Output : Type} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] [Fintype State] (sys : InformationSystem State Input Output) (s : State) (is : List Input) (hlen : Fintype.card State < is.length) : ∃ i j, i < j ∧ j ≤ is.length ∧ sys.equivalent sys (sys.eval s (List.take i is)).1 (sys.eval s (List.take j is)).1
Show details
fun {State Input Output} [Nonempty State] [Norm State] [Nonempty Input] [Norm Input] [Nonempty Output] [Norm Output] [NormNonneg State] [NormNonneg Input] [NormNonneg Output] [Fintype State] sys s is hlen => Exists.casesOn (InformationSystem.exists_repeat_state sys s is hlen) fun i h => Exists.casesOn h fun j h => And.casesOn h fun hij right => And.casesOn right fun hjlen heq => Exists.intro i (Exists.intro j ⟨hij, ⟨hjlen, Eq.mpr (id (congrArg (fun _a => sys.equivalent sys _a (sys.eval s (List.take j is)).1) heq)) fun js => Eq.refl (sys.eval (sys.eval s (List.take j is)).1 js).2⟩⟩)
Complexity: 3345 (size of the value term)
Dependencies: InformationSystem, InformationSystem.equivalent, InformationSystem.eval, NormNonneg
Proof dependencies: InformationSystem.exists_repeat_state
Mathlib dependencies: Fintype, Fintype.card, Norm
Lean core dependencies: And, Eq, Eq.mpr, Exists, List, List.length, List.take, Nat, Nonempty, congrArg, id
Used by: (none)
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