Code

Twp#10

Code

Merged

hei411 merged 21 commits intologsem:twplogsem/clutch:twpfrom hei411:twphei411/clutch:twpCopy head branch name to clipboardJan 23, 2024

+1,027-1

Commits

Commits on Jan 9, 2024

• starting to write total weakest pre

  hei411

  committed
  0694eb9

  Copy full SHA for 0694eb9

Commits on Jan 10, 2024

• First file for twp completed

  hei411

  committed
  6b53586

  Copy full SHA for 6b53586

• start working on adequacy

  hei411

  committed
  68e9aa4

  Copy full SHA for 68e9aa4

• some progress

  hei411

  committed
  605f0c0

  Copy full SHA for 605f0c0

• state lemma of another induction hypothesis for twp, it is admitted for now

  hei411

  committed
  71e3be4

  Copy full SHA for 71e3be4

• Added real_le_limit lemma

  hei411

  committed
  d2b2b80

  Copy full SHA for d2b2b80

• Added limit rules

  hei411

  committed
  230143e

  Copy full SHA for 230143e

Commits on Jan 11, 2024

• added strong fixpoint rule

  hei411

  committed
  a1c39e5

  Copy full SHA for a1c39e5

• Complete stronger induction lemma

  hei411

  committed
  45e2230

  Copy full SHA for 45e2230

• small add

  hei411

  committed
  7886b53

  Copy full SHA for 7886b53

• Small fix

  hei411

  committed
  fc60504

  Copy full SHA for fc60504

• make more progress on another induction lemma

  hei411

  committed
  efdcc0e

  Copy full SHA for efdcc0e

• Solved ind'

  hei411

  committed
  5d04db1

  Copy full SHA for 5d04db1

Commits on Jan 12, 2024

• simplify some hypothesis

  hei411

  committed
  be10159

  Copy full SHA for be10159

• translate adequacy to just pure lemmas

  hei411

  committed
  ac69142

  Copy full SHA for ac69142

• small change

  hei411

  committed
  3bced86

  Copy full SHA for 3bced86

• Completed val case

  hei411

  committed
  ac3d35d

  Copy full SHA for ac3d35d

Commits on Jan 22, 2024

• Now remaining two ugly lemmas

  hei411

  committed
  89af689

  Copy full SHA for 89af689

• COMPLETED

  hei411

  committed
  1931b32

  Copy full SHA for 1931b32

Commits on Jan 23, 2024

• ported continuity laws and prove the ones for ub_logic wp and app coupl wp

  hei411

  committed
  88ba1b3

  Copy full SHA for 88ba1b3

• Implement limit adequacy theorem for ub twp

  hei411

  committed
  c048e6d

  Copy full SHA for c048e6d