proofmode_monpred.ref 881 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
1 subgoal
  
  I : biIndex
  PROP : sbi
  P, Q : monpred.monPred I PROP
  i : I
  ============================
  "HW" : (P -∗ Q) i
  --------------------------------------∗
  (P -∗ Q) i
  
1 subgoal
  
  I : biIndex
  PROP : sbi
  P, Q : monpred.monPred I PROP
  i, j : I
  ============================
  "HW" : (P -∗ Q) j
  "HP" : P j
  --------------------------------------∗
  Q j
  
1 subgoal
  
  I : biIndex
  PROP : sbi
  P, Q : monpred.monPred I PROP
  Objective0 : Objective Q
  𝓟, 𝓠 : PROP
  ============================
  "H2" : ∀ i : I, Q i
  "H3" : 𝓟
  "H4" : 𝓠
  --------------------------------------∗
  ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
  
38 39 40 41 42 43 44 45 46 47 48
1 subgoal
  
  I : biIndex
  PROP : sbi
  FU0 : BiFUpd PROP * ()
  P, Q : monpred.monPred I PROP
  i : I
  ============================
  --------------------------------------∗
  (Q -∗ emp) i