stack pushed, stack: (p o) \/ (exists A:dom,(less o A)/\(p A)) :: nil stack top tailed: (p o) (less o C0) stack pushed, stack: (p C0) \/ (exists A:dom,(less C0 A)/\(p A)) :: (exists B:dom,(less o B)/\(p B)) :: nil stack top tailed: (p C0) false falid, stack: (exists A:dom,(less C0 A)/\(p A)) :: (exists B:dom,(less o B)/\(p B)) :: nil stack popped: (less C0 C1)/\(p C1) (less o C1) false falid, stack: (exists A:dom,(less o A)/\(p A)) :: nil stack popped: (less o C0)/\(p C0) (less C0 C1) stack pushed, stack: (p C1) \/ (exists A:dom,(less C1 A)/\(p A)) :: nil stack top tailed: (p C1) false falid, stack: (exists A:dom,(less C1 A)/\(p A)) :: nil stack popped: (less C1 C2)/\(p C2) (less o C1) (less C0 C2) false falid, stack: nil