8.3. The main model🔗

Theorem8.3.1

uses 1used by 1✓L∃∀N

The main model, from the agent a_M (one user, one session), by checked reactions and user actions:

a_M \Rightarrow^{\mathsf u}_{F_M} a \;\Longrightarrow\; \text{every } \mathsf{vocabT} \text{ of } a \text{ has distinct keys} \;\wedge\; \mathrm{KeysDistinct}(a) \;\wedge\; \#\{\text{nodes } \mathsf{shown}\,v \text{ of } a\} \le 1 .

That at least one view is shown is OPEN. The stronger statement that every session shows exactly one view is part of Shape.W2, which is defined and TESTED, not proved.

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Att, Occ, Prefs, ReachU, isShown, sessionM, sig, tableKeysDistinct; not audited: CStepM, KeysDistinct, agentM.

Lean code for Theorem8.3.1●1 theorem

theoremdefined in Miolingo/Act.lean

complete

theorem invariants_mainU {a : BD Ctl} (h : ReachU CStepM agentM a) :
  a.ctrls.all tableKeysDistinct = true ∧
    KeysDistinct a ∧ List.countP isShown a.ctrls ≤ 1

theorem invariants_mainU {a : BD Ctl}
  (h : ReachU CStepM agentM a) :
  a.ctrls.all tableKeysDistinct = true ∧
    KeysDistinct a ∧
      List.countP isShown a.ctrls ≤ 1

**(H3)** Main model, one user and one session.

Theorem8.3.2

Statement uses 3

Statement dependency previews

Preview

Theorem 8.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Two users in two sessions against one server, from the agent a_2, by checked reactions and user actions:

a_2 \Rightarrow^{\mathsf u}_{F_M} a \;\Longrightarrow\; \text{every } \mathsf{vocabT} \text{ of } a \text{ has distinct keys} \;\wedge\; \mathrm{KeysDistinct}(a) \;\wedge\; \#\{\text{nodes } \mathsf{shown}\,v \text{ of } a\} \le 2 .

The bound counts shown views over the whole agent, not one per session.

Rests on UNBRIDGED: Tm, Tm.compile; NEW: Att, Occ, Prefs, ReachU, isShown, sess, sig, tableKeysDistinct; not audited: CStepM, KeysDistinct, agent2.

Lean code for Theorem8.3.2●1 theorem

theoremdefined in Miolingo/Act.lean

complete

theorem invariants_two_sessionsU {a : BD Ctl} (h : ReachU CStepM agent2 a) :
  a.ctrls.all tableKeysDistinct = true ∧
    KeysDistinct a ∧ List.countP isShown a.ctrls ≤ 2

theorem invariants_two_sessionsU {a : BD Ctl}
  (h : ReachU CStepM agent2 a) :
  a.ctrls.all tableKeysDistinct = true ∧
    KeysDistinct a ∧
      List.countP isShown a.ctrls ≤ 2

**(H4)** Main model, two users and two sessions.