Commit a650859a authored by Christian Müller's avatar Christian Müller

presentation results

parent 0f390288
Node 0:
True
Node 5:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 10:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(J(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 1:
∀ it:T,jt:T. (A(t1)(it,jt) ↔ eq())
Node 6:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 9:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 2:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()))
Node 7:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 3:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 8:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Node 4:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))
Name: nonomitting/fixedarity10
Description: alleq
Invariant:
∀ it:T,jt:T. (B(t1)(it,jt) ↔ B(t2)(it,jt)) ∧
∀ it:T,jt:T. (D(t1)(it,jt) ↔ D(t2)(it,jt)) ∧
∀ it:T,jt:T. (G(t1)(it,jt) ↔ G(t2)(it,jt)) ∧
∀ it:T,jt:T. (A(t1)(it,jt) ↔ A(t2)(it,jt)) ∧
∀ it:T,jt:T. (E(t1)(it,jt) ↔ E(t2)(it,jt)) ∧
∀ it:T,jt:T. (I(t1)(it,jt) ↔ I(t2)(it,jt)) ∧
∀ it:T,jt:T. (H(t1)(it,jt) ↔ H(t2)(it,jt)) ∧
∀ it:T,jt:T. (F(t1)(it,jt) ↔ F(t2)(it,jt)) ∧
∀ it:T,jt:T. (J(t1)(it,jt) ↔ J(t2)(it,jt)) ∧
∀ it:T,jt:T. (C(t1)(it,jt) ↔ C(t2)(it,jt))
Model: stubborn
Result: not inductive
WF size: 10
Time: 507 ms
Proof steps: 11
Strengthenings: 0
Largest Inv: 40
Average Inv: 20
\ No newline at end of file
digraph "Invariant Labelling" {
7 -> 8 [label = "forall i:T,j:T
G(i,j) → H += (i,j);", color = red]
0 [label = "Node 0:
True"]
4 [label = "Node 4:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
8 -> 9 [label = "forall i:T,j:T
H(i,j) → I += (i,j);", color = red]
2 -> 3 [label = "forall i:T,j:T
B(i,j) → C += (i,j);", color = red]
7 [label = "Node 7:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
6 [label = "Node 6:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
2 [label = "Node 2:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()))"]
10 [label = "Node 10:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(J(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
5 [label = "Node 5:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
6 -> 7 [label = "forall i:T,j:T
F(i,j) → G += (i,j);", color = red]
9 [label = "Node 9:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
1 [label = "Node 1:
∀ it:T,jt:T. (A(t1)(it,jt) ↔ eq())"]
9 -> 10 [label = "forall i:T,j:T
I(i,j) → J += (i,j);", color = red]
10 -> 10 [label = "forall
", color = red]
8 [label = "Node 8:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
0 -> 1 [label = "forall i:T,j:T may (Some(choice0))
O(i,j) → A += (i,j);", color = red]
3 -> 4 [label = "forall i:T,j:T
C(i,j) → D += (i,j);", color = red]
5 -> 6 [label = "forall i:T,j:T
E(i,j) → F += (i,j);", color = red]
3 [label = "Node 3:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
1 -> 2 [label = "forall i:T,j:T
A(i,j) → B += (i,j);", color = red]
4 -> 5 [label = "forall i:T,j:T
D(i,j) → E += (i,j);", color = red]
}
\ No newline at end of file
digraph "Invariant Labelling" {
7 -> 8 [label = "forall i:T,j:T
G(i,j) → H += (i,j);", color = red]
0 [label = "Node 0:
True"]
4 [label = "Node 4:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
8 -> 9 [label = "forall i:T,j:T
H(i,j) → I += (i,j);", color = red]
2 -> 3 [label = "forall i:T,j:T
B(i,j) → C += (i,j);", color = red]
7 [label = "Node 7:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
6 [label = "Node 6:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
10 -> 10 [label = "forall
", color = green]
2 [label = "Node 2:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()))"]
10 [label = "Node 10:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(J(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
5 [label = "Node 5:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
6 -> 7 [label = "forall i:T,j:T
F(i,j) → G += (i,j);", color = red]
9 [label = "Node 9:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
1 [label = "Node 1:
∀ it:T,jt:T. (A(t1)(it,jt) ↔ eq())"]
9 -> 10 [label = "forall i:T,j:T
I(i,j) → J += (i,j);", color = red]
8 [label = "Node 8:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
0 -> 1 [label = "forall i:T,j:T may (Some(choice0))
O(i,j) → A += (i,j);", color = red]
3 -> 4 [label = "forall i:T,j:T
C(i,j) → D += (i,j);", color = red]
5 -> 6 [label = "forall i:T,j:T
E(i,j) → F += (i,j);", color = red]
3 [label = "Node 3:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
1 -> 2 [label = "forall i:T,j:T
A(i,j) → B += (i,j);", color = red]
4 -> 5 [label = "forall i:T,j:T
D(i,j) → E += (i,j);", color = red]
}
\ No newline at end of file
digraph "Invariant Labelling" {
6 -> 7 [label = "forall i:T,j:T
F(i,j) → G += (i,j);", color = green]
0 [label = "Node 0:
True"]
5 -> 6 [label = "forall i:T,j:T
E(i,j) → F += (i,j);", color = green]
3 -> 4 [label = "forall i:T,j:T
C(i,j) → D += (i,j);", color = green]
4 [label = "Node 4:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
9 -> 10 [label = "forall i:T,j:T
I(i,j) → J += (i,j);", color = green]
8 -> 9 [label = "forall i:T,j:T
H(i,j) → I += (i,j);", color = green]
7 [label = "Node 7:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
6 [label = "Node 6:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
4 -> 5 [label = "forall i:T,j:T
D(i,j) → E += (i,j);", color = green]
7 -> 8 [label = "forall i:T,j:T
G(i,j) → H += (i,j);", color = green]
10 -> 10 [label = "forall
", color = green]
2 [label = "Node 2:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()))"]
10 [label = "Node 10:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(J(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
5 [label = "Node 5:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
9 [label = "Node 9:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
1 [label = "Node 1:
∀ it:T,jt:T. (A(t1)(it,jt) ↔ eq())"]
8 [label = "Node 8:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
0 -> 1 [label = "forall i:T,j:T may (Some(choice0))
O(i,j) → A += (i,j);", color = red]
2 -> 3 [label = "forall i:T,j:T
B(i,j) → C += (i,j);", color = green]
3 [label = "Node 3:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
1 -> 2 [label = "forall i:T,j:T
A(i,j) → B += (i,j);", color = green]
}
\ No newline at end of file
digraph "Invariant Labelling" {
7 -> 8 [label = "forall i:T,j:T
G(i,j) → H += (i,j);", color = red]
0 [label = "Node 0:
True"]
4 [label = "Node 4:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
9 -> 10 [label = "forall i:T,j:T
I(i,j) → J += (i,j);", color = green]
8 -> 9 [label = "forall i:T,j:T
H(i,j) → I += (i,j);", color = red]
2 -> 3 [label = "forall i:T,j:T
B(i,j) → C += (i,j);", color = red]
7 [label = "Node 7:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
6 [label = "Node 6:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
10 -> 10 [label = "forall
", color = green]
2 [label = "Node 2:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()))"]
10 [label = "Node 10:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧
(D(t1)(it,jt) ↔ eq()) ∧
(G(t1)(it,jt) ↔ eq()) ∧
(A(t1)(it,jt) ↔ eq()) ∧
(E(t1)(it,jt) ↔ eq()) ∧
(I(t1)(it,jt) ↔ eq()) ∧
(H(t1)(it,jt) ↔ eq()) ∧
(F(t1)(it,jt) ↔ eq()) ∧
(J(t1)(it,jt) ↔ eq()) ∧
(C(t1)(it,jt) ↔ eq()))"]
5 [label = "Node 5:
∀ it:T,jt:T. ((B(t1)(it,jt) ↔ eq()) ∧