Download Prouveur interactif - Manuel Utilisateur

86
Prouveur interactif - Manuel Utilisateur
New Hypothesis since last command
ntt = tt$0 &
not(tt = tt$0) &
not(tt$0 = tt) &
pass(tident(tt)): ran(pass) &
pass(tident(tt)): PASSWORDS
Goal
(tconnait\/{tt$0}*tconnait[{tt}])[{tt$0}] =
{pass(tident(tt))}
End
PRI> pp
Starting Prover Predicate Call
Proved by the Predicate Prover
Current PO is fork.6
Unproved saved Unproved
Command line is
Force(0) &
pr(Red) &
dc(ntt = tt$0) &
pr(Red) &
pp &
Next
Saved line pos 1
Force(0) &
dd
Hypothesis
...
Goal
not(ntt = tt$0) =>
(tconnait\/{ntt}*tconnait[{tt}])[{tt$0}] =
{pass((tident<+{ntt|->tident(tt)})(tt$0))}
End
PRI> pr(Red)
Starting Prover Call
Current PO is fork.6
Unproved saved Unproved
Command line is
Force(0) &
pr(Red) &
dc(ntt = tt$0) &
pr(Red) &
pp &
pr(Red) &
Next
Saved line pos 1