Newer
Older
1 subgoal
PROP : sbi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
--------------------------------------□
"H" : □ (P ∨ Q)
--------------------------------------∗
Q ∨ P
1 subgoal
PROP : sbi
P, Q : PROP
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
_ : P
--------------------------------------□
Q ∨ P
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
============================
_ : P
_ : Q
--------------------------------------□
<affine> (P ∗ Q)
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
"HP" : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
--------------------------------------∗
1 subgoal
PROP : sbi
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
_ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
--------------------------------------∗
1 subgoal
PROP : sbi
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
"HP" : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
--------------------------------------∗
1 subgoal
PROP : sbi
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
_ : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
--------------------------------------∗
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP
→ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP
→ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
→ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP
-∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP
-∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
-∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
E : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP
={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset.coPset
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
PPPPPPPPPPPPPPPPP
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ