Guarded2Network.correct' at this development's concrete value type.

Everything below Guarded2Network is proved against abstract [ExprSemantics V] [SeqBuiltins V]. This file discharges both classes at V := ComputableTLAPlus.Value (ZFSet): the ExprSemantics instance is Core/ComputableTLAPlus/Semantics/Operational.lean's operational evaluator, and SeqBuiltins Value is proved here from that evaluator's Sequences/Naturals builtin rules. correct'' is correct' at that instance, and assert_no_sorry then checks the whole correctness proof carries no sorry once every class is concrete.

theorem Guarded2Network.eval_head_iff' {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model ComputableTLAPlus.Value} {M : ComputableTLAPlus.Memory ComputableTLAPlus.Value} {e : ComputablePlusCal.Expression} {τ : ComputableTLAPlus.Typ} {v : ComputableTLAPlus.Value} : ComputableTLAPlus.Operational.Eval Ξ Ω M (head τ e) v ↔ ∃ (s : ComputableTLAPlus.Value) (vs : List ComputableTLAPlus.Value), ComputableTLAPlus.Operational.Eval Ξ Ω M e s ∧ ComputableTLAPlus.Operational.IsSeq s (v :: vs)

Head(e) evaluates exactly to the first element of the sequence e denotes.

theorem Guarded2Network.eval_tail_iff' {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model ComputableTLAPlus.Value} {M : ComputableTLAPlus.Memory ComputableTLAPlus.Value} {e : ComputablePlusCal.Expression} {τ : ComputableTLAPlus.Typ} {t : ComputableTLAPlus.Value} : ComputableTLAPlus.Operational.Eval Ξ Ω M (tail τ e) t ↔ ∃ (s : ComputableTLAPlus.Value) (v : ComputableTLAPlus.Value) (vs : List ComputableTLAPlus.Value), ComputableTLAPlus.Operational.Eval Ξ Ω M e s ∧ ComputableTLAPlus.Operational.IsSeq s (v :: vs) ∧ ComputableTLAPlus.Operational.IsSeq t vs

Tail(e) evaluates exactly to the sequence of everything but the first element.

theorem Guarded2Network.eval_lenGt' {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model ComputableTLAPlus.Value} {M : ComputableTLAPlus.Memory ComputableTLAPlus.Value} {e : ComputablePlusCal.Expression} {τ : ComputableTLAPlus.Typ} {n : ℕ} {s : ComputableTLAPlus.Value} {vs : List ComputableTLAPlus.Value} (hes : ComputableTLAPlus.Operational.Eval Ξ Ω M e s) (hseq : ComputableTLAPlus.Operational.IsSeq s vs) : ∃ (b : ComputableTLAPlus.Value), ComputableTLAPlus.Operational.Eval Ξ Ω M (lenGt τ e n) b ∧ ComputableTLAPlus.Operational.IsBool b ∧ (b = ComputableTLAPlus.Value.tru ↔ n < vs.length)

Len(e) > n evaluates to a boolean whenever e is a sequence, TRUE exactly when that sequence is longer than n.

theorem Guarded2Network.eval_seq_nil_iff' {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model ComputableTLAPlus.Value} {M : ComputableTLAPlus.Memory ComputableTLAPlus.Value} {τ : ComputableTLAPlus.Typ} {s : ComputableTLAPlus.Value} : ComputableTLAPlus.Operational.Eval Ξ Ω M (ComputableTLAPlus.Expression.seq [] τ) s ↔ ComputableTLAPlus.Operational.IsSeq s []

<<>> evaluates to the empty sequence, and only that.

instance Guarded2Network.instSeqBuiltinsValue : SeqBuiltins ComputableTLAPlus.Value

The operational evaluator satisfies Guarded2Network's sequence-expression laws.

theorem Guarded2Network.correct'' {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model ComputableTLAPlus.Value} : Compiler.Correct compile (fun (s : SourceProgram ComputableTLAPlus.Value Ξ Ω) => GuardedPlusCal.Algorithm.init Ξ Ω s.algo) (NetworkPlusCal.Algorithm.init Ξ Ω)

Guarded2Network.correct' at this development's concrete value type Value (ZFSet), with the operational ExprSemantics Value instance (whose evalVar/evalSubst fields are evalVar'/ evalSubst') and the SeqBuiltins Value instance above. Ξ/Ω stay universally quantified — the statement holds for every operator environment and model.